11-14, 12:00–12:30 (Asia/Bangkok), Stage 3
hevm is a symbolic execution engine for the EVM that can prove safety properties for EVM bytecode or verify semantic equivalence between two bytecode objects. It exposes a user-friendly API in Solidity that allows you to define symbolic tests using almost exactly the same syntax as usual unit tests.
In this talk, we'll present hevm, what it's useful for, and when and how to use it to help secure your digital contracts.
Mate is a formal verification engineer at the Ethereum Foundation and occasionally does research in formal verification at various universities. He is currently working on hevm, a symbolic execution engine for finding issues with digital contracts.