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

Disgrifiad llawn

Manylion Llyfryddiaeth
Prif Awduron:	Zheng Yang, Hang Lei
Fformat:	Erthygl
Iaith:	English
Cyhoeddwyd:	IEEE 2018-01-01
Cyfres:	IEEE Access
Pynciau:	Formal verification smart contracts evaluation strategy interpreter higher-order logic theorem proving security
Mynediad Ar-lein:	https://ieeexplore.ieee.org/document/8531607/

Eitemau Tebyg

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

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

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

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

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

Automated theorem proving : a logical basis /
gan: 403272 Loveland, Donald W.
Cyhoeddwyd: (1978)

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

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

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

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

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

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

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

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

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

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

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

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

Another look at automated theorem-proving
gan: Koblitz Neal
Cyhoeddwyd: (2007-12-01)

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

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

A computational logic /
gan: 403382 Boyer, Robert S., et al.
Cyhoeddwyd: (1979)

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

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

Another look at automated theorem-proving II
gan: Koblitz Neal
Cyhoeddwyd: (2012-02-01)

A survey of smart contract formal specification and verification
gan: Tolmach, Palina, et al.
Cyhoeddwyd: (2022)

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

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

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

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

SPECIFICATION FORMALIZATION OF STATE CHARTS FOR COMPLEX SYSTEM MANAGEMENT
gan: Dmytro Nikitin
Cyhoeddwyd: (2023-07-01)

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

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

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

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

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

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

KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification
gan: Yanhong Huang, et al.
Cyhoeddwyd: (2019-01-01)

Dealing with Degeneracies in Automated Theorem Proving in Geometry
gan: Zoltán Kovács, et al.
Cyhoeddwyd: (2021-08-01)

Blockchain-enhanced smart contracts for formal verification of IoT access control mechanisms
gan: Zhifeng Guo
Cyhoeddwyd: (2025-04-01)