Watch / Building an End-to-End EVM Symbolic Execution Engine in Solidity

Building an End-to-End EVM Symbolic Execution Engine in Solidity

  • YouTube
  • Details

Building an End-to-End EVM Symbolic Execution Engine in Solidity

Duration: 00:23:15

Speaker: Leo Alt

Type: Talk

Expertise: Advanced

Event: Devcon 6

Date: Oct 2022

Symbolic execution is a widely used approach to formally verify/analyze EVM bytecode. But what exactly is it? What are constraints, and solvers?? Why do you need symbols anyway?? In this talk we will go through a symbolic execution engine for EVM bytecode fully written in Solidity, hopefully demonstrating how beautiful and simple these techniques are, and incentivizing developers to contribute to or write their own formal methods tools.
About the speakers

LA

Leo Alt

Leo is the Formal Verification Lead at the Ethereum Foundation where he also contributes to the Solidity language and compiler.

  • Related