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

被引：0
|
作者：
Yang Z. [1 ]
Lei H. [1 ]
机构：
[1] School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu
来源：
International Journal of Performability Engineering | 2019年 / 15卷 / 11期
关键词：
Coq; Formal memory framework; Higher-order logic theorem proving; Programming language;
D O I：
10.23940/ijpe.19.11.p19.29983007
中图分类号：
学科分类号：
摘要：
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.
引用
收藏
页码：2998 / 3007
页数：9
相关论文
共 50 条
  • [1] Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems
    Yang, Zheng
    Lei, Hang
    IEEE ACCESS, 2018, 6 : 70331 - 70348
  • [2] Graph Representations for Higher-Order Logic and Theorem Proving
    Paliwal, Aditya
    Loos, Sarah M.
    Rabe, Markus N.
    Bansal, Kshitij
    Szegedy, Christian
    THIRTY-FOURTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THE THIRTY-SECOND INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE AND THE TENTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2020, 34 : 2967 - 2974
  • [3] Progress in the Development of Automated Theorem Proving for Higher-Order Logic
    Sutcliffe, Geoff
    Benzmueller, Christoph
    Brown, Chad E.
    Theiss, Frank
    AUTOMATED DEDUCTION - CADE-22, 2009, 5663 : 116 - +
  • [4] Theorem Proving in Dependently-Typed Higher-Order Logic
    Rothgang, Colin
    Rabe, Florian
    Benzmueller, Christoph
    AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 438 - 455
  • [5] Formal Modeling and Verification of Function Limit in Higher-Order Logic
    Zhao C.-N.
    Zhao G.
    Jisuanji Xuebao/Chinese Journal of Computers, 2020, 43 (11): : 2119 - 2133
  • [6] Formal analysis of 2D image processing filters using higher-order logic theorem proving
    Adnan Rashid
    Sa’ed Abed
    Osman Hasan
    EURASIP Journal on Advances in Signal Processing, 2022
  • [7] Formal analysis of 2D image processing filters using higher-order logic theorem proving
    Rashid, Adnan
    Abed, Sa'ed
    Hasan, Osman
    EURASIP JOURNAL ON ADVANCES IN SIGNAL PROCESSING, 2022, 2022 (01)
  • [8] HIGHER-ORDER LOGIC THEOREM-PROVING AND ITS APPLICATIONS - SPECIAL ISSUE
    MELHAM, TF
    COMPUTER JOURNAL, 1995, 38 (02): : 89 - 90
  • [9] Tutorial: Using TPS for higher-order theorem proving and ETPS for teaching logic
    Andrews, PB
    Brown, CE
    AUTOMATED DEDUCTION - CADE-17, 2000, 1831 : 511 - 512
  • [10] Comparing approaches to resolution based higher-order theorem proving
    Benzmüller, C
    SYNTHESE, 2002, 133 (1-2) : 203 - 235
12345