Modeling and verification of smart contracts with Abstract State Machines

Abstract

Blockchain is a decentralized and distributed ledger system that records and verifies transactions across a network of computers and ensures transparency, immutability, and trustworthiness. Smart contracts are programs or protocols embedded into the distributed ledgers and are used to automate agreements between parties of a blockchain. Smart contracts are vulnerable to attacks due to their immutable and public nature, thus, it is important to guarantee the correctness of contracts already at design-time in order to avoid catastrophic events and huge loss of money.