Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems

Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems

In recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order logic theorem proving and symbolic execution for verifying the reliability and security of smart contracts developed in the Ethereum blockchain system without suffering f...

書目詳細資料
Main Authors:	Zheng Yang, Hang Lei
格式:	Article
語言:	English
出版:	IEEE 2018-01-01
叢編:	IEEE Access
主題:	Formal verification smart contracts evaluation strategy interpreter higher-order logic theorem proving security
在線閱讀:	https://ieeexplore.ieee.org/document/8531607/

相似書籍

Symbolic logic and mechanical theorem proving /
由: 336504 Chang, Chin-Ling, et al.
出版: (1973)

Formal analysis of 2D image processing filters using higher-order logic theorem proving
由: Adnan Rashid, et al.
出版: (2022-06-01)

Formal Verification of Fractional-Order PID Control Systems Using Higher-Order Logic
由: Chunna Zhao, et al.
出版: (2022-08-01)

Logic for computer science : foundations of automatic theorem proving /
由: 455116 Gallier, Jean H.
出版: (1986)

Formal verification of Matrix based MATLAB models using interactive theorem proving
由: Ayesha Gauhar, et al.
出版: (2021-03-01)

Automated theorem proving : a logical basis /
由: 403272 Loveland, Donald W.
出版: (1978)

Formal Analysis of Language-Based Android Security Using Theorem Proving Approach
由: Wilayat Khan, et al.
出版: (2019-01-01)

Theorem proving with analytic tableaux and related methods /
由: International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (4th : 1995 : St Goar, Germany), et al.
出版: (1995)

On the calculus of positively constructed formulas for authomated theorem proving
由: A. V. Davydov, et al.
出版: (2010-12-01)

A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving
由: Yassmeen Elderhalli, et al.
出版: (2019-01-01)

A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics
由: Dakai Guo, et al.
出版: (2023-05-01)

Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving
由: Adnan Rashid, et al.
出版: (2020-01-01)

Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
由: Mauricio Ayala-Rincón, et al.
出版: (2013-01-01)

A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts
由: Zheng Yang, et al.
出版: (2020-01-01)

Refinement modeling and verification of secure operating systems for communication in digital twins
由: Zhenjiang Qian, et al.
出版: (2024-04-01)

Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions /
由: 183708 Bertot, Yves, et al.
出版: (2004)

Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation
由: Haitao Wang, et al.
出版: (2021-01-01)

Pengembangan Perangkat Pembelajaran Geometri Ruang dengan Model Proving Theorem
由: Bambang Eko Susilo, et al.
出版: (2016-03-01)

FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq
由: Zheng Yang, et al.
出版: (2019-01-01)

Another look at automated theorem-proving
由: Koblitz Neal
出版: (2007-12-01)

Formal modeling and analyzing method for database security policy
由: Rong WANG, et al.
出版: (2015-09-01)

Formal modeling and analyzing method for database security policy
由: Rong WANG, et al.
出版: (2015-09-01)

A computational logic /
由: 403382 Boyer, Robert S., et al.
出版: (1979)

HOW DOES PRE-SERVICE MATHEMATICS TEACHER PROVE THE LIMIT OF A FUNCTION BY FORMAL DEFINITION?
由: Rina Oktaviyanthi, et al.
出版: (2018-06-01)

Research on formal security policy model specification and its formal analysis
由: LI Li-ping1, et al.
出版: (2006-01-01)

Research on formal security policy model specification and its formal analysis
由: LI Li-ping1, et al.
出版: (2006-01-01)

Another look at automated theorem-proving II
由: Koblitz Neal
出版: (2012-02-01)

A survey of smart contract formal specification and verification
由: Tolmach, Palina, et al.
出版: (2022)

State-of-the-art survey of smart contract verification based on formal methods
由: Wenbo ZHANG, et al.
出版: (2022-08-01)

State-of-the-art survey of smart contract verification based on formal methods
由: Wenbo ZHANG, et al.
出版: (2022-08-01)

Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
由: Ferruccio Guidi
出版: (2012-01-01)

LoET-E: A Refined Theory for Proving Security Properties of Cryptographic Protocols
由: Jiawen Song, et al.
出版: (2019-01-01)

SPECIFICATION FORMALIZATION OF STATE CHARTS FOR COMPLEX SYSTEM MANAGEMENT
由: Dmytro Nikitin
出版: (2023-07-01)

Proving, Refuting, Improving—Looking for a Theorem
由: Branislav Boričić
出版: (2022-10-01)

Automated Deduction -- CADE-21 [electronic resource] : 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings /
由: International Conference on Automated Deduction (21st : 2007 : Bremen, Germany), et al.
出版: (2007)

Toward Secure and Reliable IoT Systems: A Comprehensive Review of Formal Methods Applications
由: Ikram Haddou-Oumouloud, et al.
出版: (2024-01-01)

Modeling and verification of finite field multiplier using formal method
由: Zhang Jie, et al.
出版: (2018-01-01)

Formal Verification of Blockchain Smart Contracts via ATL Model Checking
由: Wonhong Nam, et al.
出版: (2022-01-01)

Didactical Transposition within Reflective Practice of an Indonesian Mathematics Teacher Community: A Case in Proving the Pythagorean Theorem Topic
由: Rudi Rudi, et al.
出版: (2022-03-01)

A Novel Combinational ATP Based on Contradiction Separation for First-Order Logic
由: Jian Zhong, et al.
出版: (2020-06-01)