ESOP invited speaker Mooly Sagiv
My research focuses on easing the task of developing reliable and efficient software systems. I am particularly interested in static program analysis which combines two disciplines: automated theorem proving and abstract interpretation. In the next decade, I am hoping to develop useful techniques in order to change the ways modern software is built. I am particularly interested in proof automation, given a program and a requirement, automatically prove or disprove that all executions of the program satisfy the requirements. This problem is in general undecidable and untractable.
Talk
Scaling Formal Verification to Realistic Code with Applications to DeFi Verification
Tuesday, 9:00
Room: Auditorium
Deductive verification tools like Dafny and Viper compile the program into an SMT formula and then utilize SMT solvers to find potential bugs or prove their absence. These tools are used to reason about small programs. However, these techniques do not scale due to the inherent complexity of SMT solving and the need to specify exact procedure behavior. Furthermore, common coding patterns such as nonlinear expressions, unbounded data structures and indirect storage complicates SMT reasoning.
We present the Certora Prover, a tool that checks the semantics of the executable code against its intended behavior written in a high-level declarative language for writing relational specifications, called CVL. Developer-written specifications in CVL have prevented billion-dollar mistakes and improved code security. The Certora Prover has secured 50% of the total value locked in the Ethereum blockchain. Also, specifications are written by Solidity developers and external security experts.