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

Bibliografski detalji
Glavni autori:	Zheng Yang, Hang Lei
Format:	Članak
Jezik:	English
Izdano:	IEEE 2018-01-01
Serija:	IEEE Access
Teme:	Formal verification smart contracts evaluation strategy interpreter higher-order logic theorem proving security
Online pristup:	https://ieeexplore.ieee.org/document/8531607/

Slični predmeti

Symbolic logic and mechanical theorem proving /
od: 336504 Chang, Chin-Ling, i dr.
Izdano: (1973)

Formal analysis of 2D image processing filters using higher-order logic theorem proving
od: Adnan Rashid, i dr.
Izdano: (2022-06-01)

Formal Verification of Fractional-Order PID Control Systems Using Higher-Order Logic
od: Chunna Zhao, i dr.
Izdano: (2022-08-01)

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

Formal verification of Matrix based MATLAB models using interactive theorem proving
od: Ayesha Gauhar, i dr.
Izdano: (2021-03-01)

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

Formal Analysis of Language-Based Android Security Using Theorem Proving Approach
od: Wilayat Khan, i dr.
Izdano: (2019-01-01)

Theorem proving with analytic tableaux and related methods /
od: International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (4th : 1995 : St Goar, Germany), i dr.
Izdano: (1995)

On the calculus of positively constructed formulas for authomated theorem proving
od: A. V. Davydov, i dr.
Izdano: (2010-12-01)

A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving
od: Yassmeen Elderhalli, i dr.
Izdano: (2019-01-01)

A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics
od: Dakai Guo, i dr.
Izdano: (2023-05-01)

Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving
od: Adnan Rashid, i dr.
Izdano: (2020-01-01)

Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
od: Mauricio Ayala-Rincón, i dr.
Izdano: (2013-01-01)

A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts
od: Zheng Yang, i dr.
Izdano: (2020-01-01)

Refinement modeling and verification of secure operating systems for communication in digital twins
od: Zhenjiang Qian, i dr.
Izdano: (2024-04-01)

Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions /
od: 183708 Bertot, Yves, i dr.
Izdano: (2004)

Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation
od: Haitao Wang, i dr.
Izdano: (2021-01-01)

Pengembangan Perangkat Pembelajaran Geometri Ruang dengan Model Proving Theorem
od: Bambang Eko Susilo, i dr.
Izdano: (2016-03-01)

Another look at automated theorem-proving
od: Koblitz Neal
Izdano: (2007-12-01)

Formal modeling and analyzing method for database security policy
od: Rong WANG, i dr.
Izdano: (2015-09-01)

Formal modeling and analyzing method for database security policy
od: Rong WANG, i dr.
Izdano: (2015-09-01)

A computational logic /
od: 403382 Boyer, Robert S., i dr.
Izdano: (1979)

Research on formal security policy model specification and its formal analysis
od: LI Li-ping1, i dr.
Izdano: (2006-01-01)

Research on formal security policy model specification and its formal analysis
od: LI Li-ping1, i dr.
Izdano: (2006-01-01)

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

A survey of smart contract formal specification and verification
od: Tolmach, Palina, i dr.
Izdano: (2022)

State-of-the-art survey of smart contract verification based on formal methods
od: Wenbo ZHANG, i dr.
Izdano: (2022-08-01)

State-of-the-art survey of smart contract verification based on formal methods
od: Wenbo ZHANG, i dr.
Izdano: (2022-08-01)

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

LoET-E: A Refined Theory for Proving Security Properties of Cryptographic Protocols
od: Jiawen Song, i dr.
Izdano: (2019-01-01)

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

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

Toward Secure and Reliable IoT Systems: A Comprehensive Review of Formal Methods Applications
od: Ikram Haddou-Oumouloud, i dr.
Izdano: (2024-01-01)

Automated Deduction -- CADE-21 [electronic resource] : 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings /
od: International Conference on Automated Deduction (21st : 2007 : Bremen, Germany), i dr.
Izdano: (2007)

Modeling and verification of finite field multiplier using formal method
od: Zhang Jie, i dr.
Izdano: (2018-01-01)

Didactical Transposition within Reflective Practice of an Indonesian Mathematics Teacher Community: A Case in Proving the Pythagorean Theorem Topic
od: Rudi Rudi, i dr.
Izdano: (2022-03-01)

A Novel Combinational ATP Based on Contradiction Separation for First-Order Logic
od: Jian Zhong, i dr.
Izdano: (2020-06-01)

KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification
od: Yanhong Huang, i dr.
Izdano: (2019-01-01)

Dealing with Degeneracies in Automated Theorem Proving in Geometry
od: Zoltán Kovács, i dr.
Izdano: (2021-08-01)

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