@inproceedings{f049c8daac4443fdad2bb723c3e76390,
title = "Formal specification and verification of solidity contracts with events",
abstract = "Events in the Solidity language provide a means of communication between the on-chain services of decentralized applications and the users of those services. Events are commonly used as an abstraction of contract execution that is relevant from the users{\textquoteright} perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source-level approach for the formal specification and verification of Solidity contracts with the primary focus on events. Our approach allows the specification of events in terms of the on-chain data that they track, and the predicates that define the correspondence between the blockchain state and the abstract view provided by the events. The approach is implemented in solc-verify, a modular verifier for Solidity, and we demonstrate its applicability with various examples.",
keywords = "Events, Smart contracts, Solidity, Specification, Verification",
author = "{\'A}kos Hajdu and Dejan Jovanovi{\'c} and Gabriela Ciocarlie",
note = "Publisher Copyright: {\textcopyright} {\'A}kos Hajdu, Dejan Jovanovi{\'c}, and Gabriela Ciocarlie; licensed under Creative Commons License CC-BY; 2nd Workshop on Formal Methods for Blockchains, FMBC 2020 ; Conference date: 20-07-2020 Through 21-07-2020",
year = "2020",
month = dec,
doi = "10.4230/OASIcs.FMBC.2020.2",
language = "English",
series = "OpenAccess Series in Informatics",
editor = "Bruno Bernardo and Diego Marmsoler",
booktitle = "2nd Workshop on Formal Methods for Blockchains, FMBC 2020",
}