Smart, and also Reliable and Gas-Efficient, Contracts

Abstract

A smart contract is a software program that runs on top of a blockchain. It contains a collection of public functions that can be invoked within the transactions launched over the contract by parties interacting with it. Being computer programs, well-studied formal verification techniques can be applied to them. Indeed, smart contracts are a very interesting application domain for validation, verification and optimization techniques since (1) they are relatively small in size, hence the application of these techniques scales better than when applied to larger industrial code, (2) they are valuable (in the corresponding blockchain cryptocurrency), hence software bugs or inefficiencies can cause economical losses and there is much interest in formally proving their safety and security, and (3) they require proving new specific properties to ensure their reliability and efficiency