DOI: 10.17587/prin.11.3-13

Systematic Review of Automatic Verification of Smart-Contracts

I. A. Fedotov, ivan.fedotov@phystech.edu, A. S. Khritankov, anton.khritankov@acm.org, Moscow Institute of Physics and Technology, Dolgoprudny, Moscow Region, 141701, Russian Federation

Corresponding author: Fedotov Ivan A., PhD Student, Moscow Institute of Physics and Technology, Dolgoprudny, Moscow Region, 141701, Russian Federation, E-mail: ivan.fedotov@phystech.edu

A smart contract is a special kind of software code that runs on a blockchain platform. As other software smart contracts can contain errors and vulnerabilities that could lead to substantial adverse results and financial losses. These risks are compounded by the growing popularity of blockchain-based systems, devices, and infrastructure in finance, legal, energy and other domains. Early detection of software errors can reduce losses and automatic verification tools are a method of choice for situations where reliability and security is important. This systematic review analyzes the state of the art in smart contracts verification in 2015—2019. The review gives a brief introduction to blockchain, smart contracts and decentralized applications (dApps), examines verification methods for smart contracts and related tools. Different verification methods are taken into account including formal verification, dynamic and static code analysis, deductive analysis, theorem provers tools, code and execution trace audit. The following research questions have been considered:

• What code verification methodologies are commonly applied to software verification?
• Which of them are applicable to smart contracts and what tools are available?
• What are current limitations in smart contract verification?
• What are possible future directions in smart contract verification?

During the research process more than 100 academic papers and industrial reports, software tool documentation and guides were studied. As a result, 52 studies, basically in English, were included in the systematic review.

Keywords: smart-contract, blockchain, verification, systematic review, Ethereum, BitCoin, model checking

pp. 3–13

For citation:
Fedotov I. A., Khritankov A. S. Systematic Review of Automatic Verification of Smart-Contracts, Programmnaya Ingeneria, 2020, vol. 11, no. 1, pp. 3—13.