DROPS

Document

Short Paper

DOI: 10.4230/OASIcs.FMBC.2020.2

Formal Specification and Verification of Solidity Contracts with Events (Short Paper)

Authors: Ákos Hajdu, Dejan Jovanović, and Gabriela Ciocarlie

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

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' 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.

Cite as

Ákos Hajdu, Dejan Jovanović, and Gabriela Ciocarlie. Formal Specification and Verification of Solidity Contracts with Events (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hajdu_et_al:OASIcs.FMBC.2020.2,
  author =	{Hajdu, \'{A}kos and Jovanovi\'{c}, Dejan and Ciocarlie, Gabriela},
  title =	{{Formal Specification and Verification of Solidity Contracts with Events}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{2:1--2:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.2},
  URN =		{urn:nbn:de:0030-drops-134153},
  doi =		{10.4230/OASIcs.FMBC.2020.2},
  annote =	{Keywords: Smart contracts, Solidity, events, specification, verification}
}

Search Results

Documents authored by Jovanović, Dejan

Formal Specification and Verification of Solidity Contracts with Events (Short Paper)

Abstract

Cite as

Thanks for your feedback!

Could not send message