@inproceedings{3608e57a9a264113824d6e633587e2d7,
title = "Smart contract interactions in coq",
abstract = "We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) and breadth-first execution blockchains (like Tezos). We represent smart contracts programs in Coq{\textquoteright}s functional language Gallina, enabling easier reasoning about functional correctness of concrete contracts than other approaches. In particular we develop a Congress contract in this style. This contract – a simplified version of the infamous DAO – is interesting because of its very dynamic communication pattern with other contracts. We give a high-level partial specification of the Congress{\textquoteright}s behavior, related to reentrancy, and prove that the Congress satisfies it for all possible smart contract execution orders.",
keywords = "Blockchain, Coq, Formal verification, Smart contracts",
author = "Nielsen, {Jakob Botsch} and Bas Spitters",
year = "2020",
month = jan,
doi = "10.1007/978-3-030-54994-7_29",
language = "English",
isbn = "9783030549930",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "380--391",
editor = "Emil Sekerinski and Nelma Moreira and Oliveira, {Jos{\'e} N.} and Daniel Ratiu and Riccardo Guidotti and Marie Farrell and Matt Luckcuck and Diego Marmsoler and Jos{\'e} Campos and Troy Astarte and Laure Gonnord and Antonio Cerone and Luis Couto and Brijesh Dongol and Martin Kutrib and Pedro Monteiro and David Delmas",
booktitle = "Formal Methods- FM 2019 International Workshops - Revised Selected Papers",
address = "Netherlands",
note = "3rd World Congress on Formal Methods, FM 2019 ; Conference date: 07-10-2019 Through 11-10-2019",
}