Compositional Verification of Smart Contracts Through Communication Abstraction
summary
Claims a local bundle abstraction that reduces Solidity contracts with 2^160 addresses to a few representative users (example: 2^160 → 4) and turns parameterized verification into a sequential analysis. Implements PTGBuilder to compute representatives and SmartACE backed by the Solidity compiler and SeaHorn for checking. Evaluation vs VerX: 8 of 13 benchmarks directly supported, 12 of 13 verifiable with effort, and SmartACE yields ≥10× speedups on 10 of 12 tests.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:23Motivation: What is a smart contract
- 1:32Motivation: Trust via Source Code Verification
- 3:05Notation: States and Traces
- 6:10Challenge: Intractable Verification Problems
- 7:09Challenges: Current Solutions
- 9:08Approach: Our Insight
- 10:46Approach: A short example
- 12:13Approach: Technical Details
- 13:10Key Results of the VerX Case Study
- 14:03Conclusions
related talks
29mCompositional Verification of Smart Contracts Through Communication Abstraction
21mPractical Verification Of Smart Contracts Using Memory Splitting
25mBehavioral simulation for smart contracts
23mGradual Verification for Smart Contracts
42mTotal Smart Contracts in Pact: Model-Verified Interfaces and Governance
30mConstructing Trustworthy Smart Contracts
04mInterview
49mAlgorand Smart Contract Architecture