Watch / Using Solidity's SMTChecker

Using Solidity's SMTChecker

  • YouTube
  • IPFS
  • Details

Using Solidity's SMTChecker

Duration: 00:25:41

Speaker: Leonardo Alt

Type: Talk

Expertise: Intermediate

Event: Devcon 4

Date: Oct 2018

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.



About the speakers


Leonardo Alt

Works on Solidity and formal verification.

  • Related