A general formal memory framework for smart contracts verification based on higher-order logic theorem proving

Blockchain technology is one of the newest technologies in computer science and has been employed in many important fields. The correctness verification of smart contracts must be protected by the most reliable technology. One of the most reliable methods for s the security and reliability of smart contracts is a formal symbolic virtual machine based on higher-order logic proof system. Therefore, the present work proposes a formal specification framework of memory architecture as the basis for the symbolic execution and theorem proving combination. The framework is independent and customizable. It formalizes logic addresses, nonintrusive application programming interfaces, physical memory structures, and auxiliary tools in Coq. Simple case studies are employed to demonstrate its effectiveness. Finally, the proposed GERM framework is verified in Coq. © 2019 Totem Publisher, Inc. All rights reserved.