Trust but Verify: Scaling Deductive Verification with Abstract Interpretation - N40AI'24

Explore the challenges and solutions in scaling deductive verification for complex smart contract code through a 50-minute conference talk presented at ACM SIGPLAN. Delve into the Certora Prover's approach to formally verifying high-level functional correctness properties of low-level smart contracts using automated techniques. Learn about a unique pointer analysis algorithm developed to overcome verification challenges in large and complex programs, and how it has uncovered security errors in the Solidity compiler while significantly speeding up formal verification. Examine the specific challenges posed by memory management strategies in EVM bytecode and their impact on analysis. Gain insights from five years of experience at Certora and discover new static analysis problems arising from the increasing popularity of low-level languages like EVM bytecode and WebAssembly.