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

Полное описание

Библиографические подробности
Главные авторы:	Zheng Yang, Hang Lei
Формат:	Статья
Язык:	English
Опубликовано:	IEEE 2018-01-01
Серии:	IEEE Access
Предметы:	Formal verification smart contracts evaluation strategy interpreter higher-order logic theorem proving security
Online-ссылка:	https://ieeexplore.ieee.org/document/8531607/

Схожие документы

Symbolic logic and mechanical theorem proving /
по: 336504 Chang, Chin-Ling, и др.
Опубликовано: (1973)

Formal analysis of 2D image processing filters using higher-order logic theorem proving
по: Adnan Rashid, и др.
Опубликовано: (2022-06-01)

Formal Verification of Fractional-Order PID Control Systems Using Higher-Order Logic
по: Chunna Zhao, и др.
Опубликовано: (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, и др.
Опубликовано: (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, и др.
Опубликовано: (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), и др.
Опубликовано: (1995)

On the calculus of positively constructed formulas for authomated theorem proving
по: A. V. Davydov, и др.
Опубликовано: (2010-12-01)

A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving
по: Yassmeen Elderhalli, и др.
Опубликовано: (2019-01-01)

A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics
по: Dakai Guo, и др.
Опубликовано: (2023-05-01)

Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving
по: Adnan Rashid, и др.
Опубликовано: (2020-01-01)

Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
по: Mauricio Ayala-Rincón, и др.
Опубликовано: (2013-01-01)

A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts
по: Zheng Yang, и др.
Опубликовано: (2020-01-01)

Refinement modeling and verification of secure operating systems for communication in digital twins
по: Zhenjiang Qian, и др.
Опубликовано: (2024-04-01)

Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions /
по: 183708 Bertot, Yves, и др.
Опубликовано: (2004)

Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation
по: Haitao Wang, и др.
Опубликовано: (2021-01-01)

Pengembangan Perangkat Pembelajaran Geometri Ruang dengan Model Proving Theorem
по: Bambang Eko Susilo, и др.
Опубликовано: (2016-03-01)

Another look at automated theorem-proving
по: Koblitz Neal
Опубликовано: (2007-12-01)

Formal modeling and analyzing method for database security policy
по: Rong WANG, и др.
Опубликовано: (2015-09-01)

Formal modeling and analyzing method for database security policy
по: Rong WANG, и др.
Опубликовано: (2015-09-01)

A computational logic /
по: 403382 Boyer, Robert S., и др.
Опубликовано: (1979)

Research on formal security policy model specification and its formal analysis
по: LI Li-ping1, и др.
Опубликовано: (2006-01-01)

Research on formal security policy model specification and its formal analysis
по: LI Li-ping1, и др.
Опубликовано: (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, и др.
Опубликовано: (2022)

Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
по: Ferruccio Guidi
Опубликовано: (2012-01-01)

State-of-the-art survey of smart contract verification based on formal methods
по: Wenbo ZHANG, и др.
Опубликовано: (2022-08-01)

State-of-the-art survey of smart contract verification based on formal methods
по: Wenbo ZHANG, и др.
Опубликовано: (2022-08-01)

LoET-E: A Refined Theory for Proving Security Properties of Cryptographic Protocols
по: Jiawen Song, и др.
Опубликовано: (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)

Toward Secure and Reliable IoT Systems: A Comprehensive Review of Formal Methods Applications
по: Ikram Haddou-Oumouloud, и др.
Опубликовано: (2024-01-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), и др.
Опубликовано: (2007)

Didactical Transposition within Reflective Practice of an Indonesian Mathematics Teacher Community: A Case in Proving the Pythagorean Theorem Topic
по: Rudi Rudi, и др.
Опубликовано: (2022-03-01)

A Novel Combinational ATP Based on Contradiction Separation for First-Order Logic
по: Jian Zhong, и др.
Опубликовано: (2020-06-01)

Dealing with Degeneracies in Automated Theorem Proving in Geometry
по: Zoltán Kovács, и др.
Опубликовано: (2021-08-01)

Blockchain-enhanced smart contracts for formal verification of IoT access control mechanisms
по: Zhifeng Guo
Опубликовано: (2025-04-01)

Automated Reasoning with Analytic Tableaux and Related Methods [electronic resource] : 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007: Proceedings /
по: TABLEAUX 2007 (2007 : Aix en Provence, France), и др.
Опубликовано: (2007)

Automated technology for verification and analysis : 5th international symposium, ATVA 2007 Tokyo, Japan, October 22-25, 2007 proceedings /
по: Namjoshi, Kedar S., и др.
Опубликовано: (2007)