Int J Performability Eng ›› 2019, Vol. 15 ›› Issue (11): 2998-3007.doi: 10.23940/ijpe.19.11.p19.29983007

Previous Articles     Next Articles

A General Formal Memory Framework for Smart Contracts Verification based on Higher-Order Logic Theorem Proving

Zheng Yang* and Hang Lei   

  1. School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, 610054, China
  • Submitted on ; Revised on ; Accepted on
  • Contact: * E-mail address: zyang.uestc@gmail.com

Abstract: 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.

Key words: formal memory framework, programming language, higher-order logic theorem proving, Coq