Learn about VerX, a tool for safety verification of smart contracts, in this 15-minute IEEE conference talk. Explore functional correctness, requirements formalization, and the VerX specification language. Discover the challenges in specifying smart contract behavior and understand the concept of effective external callback freedom. Dive into the verification recipe, including delayed predicate abstraction and symbolic execution. Gain insights into automated formal verification techniques for ensuring the safety and reliability of smart contracts.
Overview
Syllabus
Intro
Motivation
Functional correctness
Correctness of Smart contract
Requirements formalization
VerX specification language
Specification challenge
Effective external callback freedom
Verification recipe
Delayed predicate abstraction
Symbolic execution + predicate abstraction
Automated formal verification with VerX
Taught by
IEEE Symposium on Security and Privacy
