Compositional Verification of Smart Contracts Through Communication Abstraction
summary
Claims that local bundles reduce contracts with 2^160 addresses to a sequential C model with a handful of representative users computed via static analysis (participation classes and a PTG-style algorithm), require a short manual or default summary per representative, and are relatively complete for parameterized safety. Implementation in SMARTACE generates C programs amenable to off-the-shelf sequential analyzers and yields order-of-magnitude speedups (examples: verification in ~26s versus >20,000s) while reducing instances to 10–16 representative users.
AI-written summary · about
chapters (9)
- 0:00Smart contract verification intro
- 2:13Smart contracts and FSMs
- 7:27Verification challenges
- 11:39Scalability in verification
- 16:34User interaction abstraction
- 20:47Evaluation vs state-of-the-art
- 23:38Extensions and limitations
- 25:24Compositional verification summary
- 26:17Q&A
related talks
15mCompositional Verification of Smart Contracts Through Communication Abstraction
21mPractical Verification Of Smart Contracts Using Memory Splitting
42mTotal Smart Contracts in Pact: Model-Verified Interfaces and Governance
23mGradual Verification for Smart Contracts
34mCost Analysis of Smart Contracts via Parametric Resource Analysis
04mInterview
25mCommSec D2 - Smart Contract (In)Security
16mSpecifying Smart Contract with Hax and ConCert