Behavioral simulation for smart contracts
summary
Automated method claims to verify unannotated smart contracts by synthesizing behavioral refinement as simulation relations between a few manually annotated reference contracts and many targets. The prototype builds synchronized product contracts, generates positive/negative examples on a private chain (Ganache), learns separators with a modified PIE learner, and checks inductiveness with a Boogie-based verifier. Empirical result: out of 41 target contracts, 35 yield verified simulations, three reveal incompatibilities (likely bugs), and three need loop variants to discharge proofs.
AI-written summary · about
chapters (5)
- 0:00Smart contract simulation intro
- 3:54Simulation synthesis core idea
- 14:54Experimental results & conclusions
- 15:59Q&A
- 25:10Closing remarks
related talks
54mProperty Based Testing - Smart testing of smart contracts
30mVerifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
33mAudit-Driven Signature Tracing for Smart Contract Safety
15mCompositional Verification of Smart Contracts Through Communication Abstraction
46mFormal verification of C# smart contracts
27mAutomated Learning and Verification of Embedded Security Architectures
14mRich Specifications for Ethereum Smart Contract Verification
23mGradual Verification for Smart Contracts