Model checking smart contracts for Ethereum

One important promise of the blockchain technology is the concept of smart contracts. They offer means for the secure execution of procedures that no entity can manipulate. This enables applications like the automation of business processes, i.e. entire business relationships in peer-to-peer collaborations can be automated securely. While the blockchain guarantees proper execution it assures the correctness of business collaboration. Since a smart contract cannot be easily changed or updated once instantiated, one has to be absolutely sure that the program code works as expected. This paper presents our tool chain that comprises the formalization of the semantics of smart contracts, via a functional specification of blockchain operations towards a formal representation of the smart contract at question, that can be formally analyzed for correct implementation via model checking.