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

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Zheng Yang, Hang Lei
Formáid:	Alt
Teanga:	English
Foilsithe / Cruthaithe:	IEEE 2018-01-01
Sraith:	IEEE Access
Ábhair:	Formal verification smart contracts evaluation strategy interpreter higher-order logic theorem proving security
Rochtain ar líne:	https://ieeexplore.ieee.org/document/8531607/

Míreanna comhchosúla

Symbolic logic and mechanical theorem proving /
de réir: 336504 Chang, Chin-Ling, et al.
Foilsithe / Cruthaithe: (1973)

Formal analysis of 2D image processing filters using higher-order logic theorem proving
de réir: Adnan Rashid, et al.
Foilsithe / Cruthaithe: (2022-06-01)

Formal Verification of Fractional-Order PID Control Systems Using Higher-Order Logic
de réir: Chunna Zhao, et al.
Foilsithe / Cruthaithe: (2022-08-01)

Logic for computer science : foundations of automatic theorem proving /
de réir: 455116 Gallier, Jean H.
Foilsithe / Cruthaithe: (1986)

Formal verification of Matrix based MATLAB models using interactive theorem proving
de réir: Ayesha Gauhar, et al.
Foilsithe / Cruthaithe: (2021-03-01)

Automated theorem proving : a logical basis /
de réir: 403272 Loveland, Donald W.
Foilsithe / Cruthaithe: (1978)

Formal Analysis of Language-Based Android Security Using Theorem Proving Approach
de réir: Wilayat Khan, et al.
Foilsithe / Cruthaithe: (2019-01-01)

Theorem proving with analytic tableaux and related methods /
de réir: International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (4th : 1995 : St Goar, Germany), et al.
Foilsithe / Cruthaithe: (1995)

On the calculus of positively constructed formulas for authomated theorem proving
de réir: A. V. Davydov, et al.
Foilsithe / Cruthaithe: (2010-12-01)

A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving
de réir: Yassmeen Elderhalli, et al.
Foilsithe / Cruthaithe: (2019-01-01)

A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics
de réir: Dakai Guo, et al.
Foilsithe / Cruthaithe: (2023-05-01)

Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving
de réir: Adnan Rashid, et al.
Foilsithe / Cruthaithe: (2020-01-01)

Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
de réir: Mauricio Ayala-Rincón, et al.
Foilsithe / Cruthaithe: (2013-01-01)

A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts
de réir: Zheng Yang, et al.
Foilsithe / Cruthaithe: (2020-01-01)

Refinement modeling and verification of secure operating systems for communication in digital twins
de réir: Zhenjiang Qian, et al.
Foilsithe / Cruthaithe: (2024-04-01)

Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions /
de réir: 183708 Bertot, Yves, et al.
Foilsithe / Cruthaithe: (2004)

Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation
de réir: Haitao Wang, et al.
Foilsithe / Cruthaithe: (2021-01-01)

Pengembangan Perangkat Pembelajaran Geometri Ruang dengan Model Proving Theorem
de réir: Bambang Eko Susilo, et al.
Foilsithe / Cruthaithe: (2016-03-01)

Another look at automated theorem-proving
de réir: Koblitz Neal
Foilsithe / Cruthaithe: (2007-12-01)

Formal modeling and analyzing method for database security policy
de réir: Rong WANG, et al.
Foilsithe / Cruthaithe: (2015-09-01)

Formal modeling and analyzing method for database security policy
de réir: Rong WANG, et al.
Foilsithe / Cruthaithe: (2015-09-01)

A computational logic /
de réir: 403382 Boyer, Robert S., et al.
Foilsithe / Cruthaithe: (1979)

Research on formal security policy model specification and its formal analysis
de réir: LI Li-ping1, et al.
Foilsithe / Cruthaithe: (2006-01-01)

Research on formal security policy model specification and its formal analysis
de réir: LI Li-ping1, et al.
Foilsithe / Cruthaithe: (2006-01-01)

Another look at automated theorem-proving II
de réir: Koblitz Neal
Foilsithe / Cruthaithe: (2012-02-01)

A survey of smart contract formal specification and verification
de réir: Tolmach, Palina, et al.
Foilsithe / Cruthaithe: (2022)

State-of-the-art survey of smart contract verification based on formal methods
de réir: Wenbo ZHANG, et al.
Foilsithe / Cruthaithe: (2022-08-01)

State-of-the-art survey of smart contract verification based on formal methods
de réir: Wenbo ZHANG, et al.
Foilsithe / Cruthaithe: (2022-08-01)

Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
de réir: Ferruccio Guidi
Foilsithe / Cruthaithe: (2012-01-01)

LoET-E: A Refined Theory for Proving Security Properties of Cryptographic Protocols
de réir: Jiawen Song, et al.
Foilsithe / Cruthaithe: (2019-01-01)

SPECIFICATION FORMALIZATION OF STATE CHARTS FOR COMPLEX SYSTEM MANAGEMENT
de réir: Dmytro Nikitin
Foilsithe / Cruthaithe: (2023-07-01)

Proving, Refuting, Improving—Looking for a Theorem
de réir: Branislav Boričić
Foilsithe / Cruthaithe: (2022-10-01)

Toward Secure and Reliable IoT Systems: A Comprehensive Review of Formal Methods Applications
de réir: Ikram Haddou-Oumouloud, et al.
Foilsithe / Cruthaithe: (2024-01-01)

Automated Deduction -- CADE-21 [electronic resource] : 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings /
de réir: International Conference on Automated Deduction (21st : 2007 : Bremen, Germany), et al.
Foilsithe / Cruthaithe: (2007)

Modeling and verification of finite field multiplier using formal method
de réir: Zhang Jie, et al.
Foilsithe / Cruthaithe: (2018-01-01)

Didactical Transposition within Reflective Practice of an Indonesian Mathematics Teacher Community: A Case in Proving the Pythagorean Theorem Topic
de réir: Rudi Rudi, et al.
Foilsithe / Cruthaithe: (2022-03-01)

A Novel Combinational ATP Based on Contradiction Separation for First-Order Logic
de réir: Jian Zhong, et al.
Foilsithe / Cruthaithe: (2020-06-01)

KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification
de réir: Yanhong Huang, et al.
Foilsithe / Cruthaithe: (2019-01-01)

Dealing with Degeneracies in Automated Theorem Proving in Geometry
de réir: Zoltán Kovács, et al.
Foilsithe / Cruthaithe: (2021-08-01)

Blockchain-enhanced smart contracts for formal verification of IoT access control mechanisms
de réir: Zhifeng Guo
Foilsithe / Cruthaithe: (2025-04-01)