VerX: Safety Verification of Smart Contracts
Offered By: IEEE via YouTube
Course Description
Overview
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.
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
Tags
Related Courses
Formal Software VerificationUniversity System of Maryland via edX Software Analysis & Testing
Georgia Institute of Technology via Udacity Computer Systems Security
Massachusetts Institute of Technology via MIT OpenCourseWare Reverse Engineering 3201: Symbolic Analysis
OpenSecurityTraining2 via Independent angr: Binary Analysis Framework - Demonstration and Analysis
New York University (NYU) via YouTube