@inproceedings {fmbc2020, title = {Formal Specification and Verification of Solidity Contracts with Events (short paper)}, booktitle = {2nd Workshop on Formal Methods for Blockchains}, year = {2020}, note = {(In press)}, type = {Workshop}, 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\&$\#$39; 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 specification of events in terms of the on-chain data that they track, and 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 = {modular verification, smart contracts}, author = {{\'A}kos Hajdu and Jovanovi{\'c}, Dejan and Ciocarlie, Gabriela} }