Formal Verification of Smart Contracts Based on Model Checking: An Overview

Abstract

Focusing on important features in blockchain applications, smart contracts are one of the most studied in the literature. Despite the trusted implementations that smart contracts offer, different security problems and vulnerabilities are rising during their development and execution. Trying to deal with such issues, different researches are proposed to give eventual solutions. Such studies focus on the verification of smart contracts and adopt different techniques. While various formal methods are considered significant effective to ensure the trustworthiness and correctness of smart contracts, this work deals with formal verification of smart contracts using model checking. In this survey, we conduct an overview on smart contracts verification using model checking. We analyze and classify each study according to four main aspects; the adopted formalism, the verified properties, the system under verification and to which blockchain platform the contribution is dedicated. Finally, we suggest some promising future directions to stir research efforts into this area.