This course focuses on teaching safety verification of smart contracts, including topics such as functional correctness, requirements formalization, and the VerX specification language. Students will learn skills such as effective external callback freedom, verification recipe, delayed predicate abstraction, symbolic execution, and automated formal verification with VerX. The teaching method includes theoretical explanations, practical examples, and hands-on exercises. This course is intended for individuals interested in smart contract development, blockchain technology, and software verification.
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
