Paper Info
Title
Behavioral simulation for smart contracts
Abstract
While smart contracts have the potential to revolutionize many important applications like banking, trade, and supply-chain, their reliable deployment begs for rigorous formal verification. Since most smart contracts are not annotated with formal specifications, general verification of functional properties is impeded. In this work, we propose an automated approach to verify unannotated smart contracts against specifications ascribed to a few manually-annotated contracts. In particular, we propose a notion of behavioral refinement, which implies inheritance of functional properties. Furthermore, we propose an automated approach to inductive proof, by synthesizing simulation relations on the states of related contracts. Empirically, we demonstrate that behavioral simulations can be synthesized automatically for several ubiquitous classes like tokens, auctions, and escrow, thus enabling the verification of unannotated contracts against functional specifications.
Year
DOI
Venue
2020
10.1145/3385412.3386022
PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation London UK June, 2020
Keywords
DocType
ISBN
Blockchain, Smart contracts, Refinement, Simulation
Conference
978-1-4503-7613-6
Citations 
PageRank 
References 
0
0.34
0
Authors
4
Name
Order
Citations
PageRank
Sidi Mohamed Beillahi100.34
Gabriela Ciocarlie210.69
Michael Emmi336521.76
Constantin Enea424926.95