@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 = {<p>
	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.</p>
},
	keywords = {modular verification, smart contracts},
	author = {{\'A}kos Hajdu and Jovanovi{\'c}, Dejan and Ciocarlie, Gabriela}
}
