Using Solidity's SMTChecker by Leonardo Alt (Devcon4)

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more. https://archive.devcon.org/archive/watch/4/using-soliditys-smtchecker Solidity's SMTChecker is a formal verification module that automatically tries to prove safety properties in Solidity smart contracts. These properties include checks for underflow, overflow, trivial conditions, unreachable code and user defined assertions. The checks are performed statically during compilation time, and the properties are either proved correct or a counterexample representing a bug is given to the user. Formal specifications for user defined properties are written using constructs already available in the language, therefore not requiring learning a new verification language/framework. If the formal specification is inaccurate or wrong, proofs are useless to the developer. Therefore, it is important to write specifications in a way that the target properties do represent the program logic. For the advanced user, some understanding about the SMTChecker may lead to specifications that also increase the module's efficiency and proving power. This talk gives an overview of the available features in Solidity's SMTChecker, and presents some insights on writing better formal specifications. Speaker(s): Leonardo Alt Skill level: Intermediate Track: Security Keywords: formal verification, safety, formal specification Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum Learn more about devcon: https://www.devcon.org/ Learn more about ethereum: https://ethereum.org/ Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. Devcon 4 was held in Prague, Czech Republic on Oct 30 - Nov 2, 2018. Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/