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

Deskribapen osoa

Xehetasun bibliografikoak
Egile Nagusiak:	Zheng Yang, Hang Lei
Formatua:	Artikulua
Hizkuntza:	English
Argitaratua:	IEEE 2018-01-01
Saila:	IEEE Access
Gaiak:	Formal verification smart contracts evaluation strategy interpreter higher-order logic theorem proving security
Sarrera elektronikoa:	https://ieeexplore.ieee.org/document/8531607/

Antzeko izenburuak

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Another look at automated theorem-proving
nork: Koblitz Neal
Argitaratua: (2007-12-01)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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