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
オンライン･アクセス:	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)

FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq
著者:: Zheng Yang, 等
出版事項: (2019-01-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)

HOW DOES PRE-SERVICE MATHEMATICS TEACHER PROVE THE LIMIT OF A FUNCTION BY FORMAL DEFINITION?
著者:: Rina Oktaviyanthi, 等
出版事項: (2018-06-01)

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)

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)

Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
著者:: Ferruccio Guidi
出版事項: (2012-01-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)

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)

Toward Secure and Reliable IoT Systems: A Comprehensive Review of Formal Methods Applications
著者:: Ikram Haddou-Oumouloud, 等
出版事項: (2024-01-01)

Modeling and verification of finite field multiplier using formal method
著者:: Zhang Jie, 等
出版事項: (2018-01-01)

Formal Verification of Blockchain Smart Contracts via ATL Model Checking
著者:: Wonhong Nam, 等
出版事項: (2022-01-01)

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)