PV0 ⊧ SolCMC

Application domain/field

• Smart contracts
• Model checking
• Symbolic model checking

Type of tool

Model checker

Expected input

Solidity program with assert statements

Format:

Solidity language SolCMC uses the asserts and requires clauses to identify verification targets.

Expected output

Reports violations of:

• Assertions
• Popping empty arrays
• Out of bounds index accesses
• Arithmetic underflow/overflow
• Division by zero
• Insufficient transfer balance.

Internals

SolCMC supports unbounded model checking as well as bounded model checking. It encodes a smart contract as a system of constrained horn clauses for unbounded model checking. It is encoded in SMT queries for bounded model checking. It uses Spacer and Eldarica. It uses cvc5 and Z3 for bounded model checking.

Comments

Shipped with Ethereum Foundation's Solidity compiler. Used to be called SMTChecker.