Automated Synthesis of External Unknown Functions

The SMTChecker, a formal verification module built-in the Solidity compiler, received a lot of improvements in 2020. Many improvements are related to Solidity‚Äôs language features, such as structs, ABI, hash and math functions, and other important features that were unsupported. When running the tool, the user now has more control and is able to set a timeout per query and choose engines separately between BMC and CHC. The CHC engine encodes Solidity code as Constrained Horn Clauses and is often... [Read More]

Symbolic Execution With ds-test

The latest release of hevm incorporates the recently introduced symbolic execution features into its unit testing framework. This lets smart contract developers formulate and prove properties in Solidity using the dapp development framework. Formally verifying properties should now be no harder than writing a property based test. In fact, it uses almost the exact same syntax! As an example, the following is a proof of the distributive property for EVM addition and multiplication: function prove_distributivity(uint x, uint y, uint z)... [Read More]

Symbolic execution for hevm

The latest release of hevm introduces symbolic execution features which can be used for checking smart contracts for correctness, step through the execution space of live contracts, or prove equivalence between them. In this tutorial we will show how to use the new capabilities of hevm, and discuss some of its unique features as a symbolic execution engine. Table of Contents About hevm Symbolic Execution and Formal Verification How does it work? Installation Using hevm symbolic Executing against live contracts... [Read More]