Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Fri 19 Jun 2020 10:00 - 10:20 at PLDI Research Papers live stream - Smart Contracts Chair(s): Ilya Sergey

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 \emph{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.

Fri 19 Jun
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

09:20 - 10:20: PLDI Research Papers - Smart Contracts at PLDI Research Papers live stream
Chair(s): Ilya SergeyYale-NUS College and National University of Singapore

YouTube lightning session video

pldi-2020-papers09:20 - 09:40
Ao LiUniversity of Toronto, Canada, Jemin Andrew ChoiUniversity of Toronto, Canada, Fan LongUniversity of Toronto, Canada
pldi-2020-papers09:40 - 10:00
Lexi BrentInternational Computer Science Institute, USA / University of Sydney, Australia, Neville GrechUniversity of Athens, Greece, Sifis LagouvardosUniversity of Athens, Greece, Bernhard ScholzUniversity of Sydney, Australia, Yannis SmaragdakisUniversity of Athens, Greece
pldi-2020-papers10:00 - 10:20
Sidi Mohamed BeillahiIRIF - Université de Paris, Gabriela CiocarlieSRI International, Michael EmmiAmazon Web Services, Constantin EneaUniversity of Paris Diderot, France