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

Detaylı Bibliyografya
Asıl Yazarlar:	Zheng Yang, Hang Lei
Materyal Türü:	Makale
Dil:	English
Baskı/Yayın Bilgisi:	IEEE 2018-01-01
Seri Bilgileri:	IEEE Access
Konular:	Formal verification smart contracts evaluation strategy interpreter higher-order logic theorem proving security
Online Erişim:	https://ieeexplore.ieee.org/document/8531607/

Benzer Materyaller

Symbolic logic and mechanical theorem proving /
Yazar:: 336504 Chang, Chin-Ling, ve diğerleri
Baskı/Yayın Bilgisi: (1973)

Formal analysis of 2D image processing filters using higher-order logic theorem proving
Yazar:: Adnan Rashid, ve diğerleri
Baskı/Yayın Bilgisi: (2022-06-01)

Formal Verification of Fractional-Order PID Control Systems Using Higher-Order Logic
Yazar:: Chunna Zhao, ve diğerleri
Baskı/Yayın Bilgisi: (2022-08-01)

Logic for computer science : foundations of automatic theorem proving /
Yazar:: 455116 Gallier, Jean H.
Baskı/Yayın Bilgisi: (1986)

Formal verification of Matrix based MATLAB models using interactive theorem proving
Yazar:: Ayesha Gauhar, ve diğerleri
Baskı/Yayın Bilgisi: (2021-03-01)

Automated theorem proving : a logical basis /
Yazar:: 403272 Loveland, Donald W.
Baskı/Yayın Bilgisi: (1978)

Formal Analysis of Language-Based Android Security Using Theorem Proving Approach
Yazar:: Wilayat Khan, ve diğerleri
Baskı/Yayın Bilgisi: (2019-01-01)

Theorem proving with analytic tableaux and related methods /
Yazar:: International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (4th : 1995 : St Goar, Germany), ve diğerleri
Baskı/Yayın Bilgisi: (1995)

On the calculus of positively constructed formulas for authomated theorem proving
Yazar:: A. V. Davydov, ve diğerleri
Baskı/Yayın Bilgisi: (2010-12-01)

A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving
Yazar:: Yassmeen Elderhalli, ve diğerleri
Baskı/Yayın Bilgisi: (2019-01-01)

A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics
Yazar:: Dakai Guo, ve diğerleri
Baskı/Yayın Bilgisi: (2023-05-01)

Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving
Yazar:: Adnan Rashid, ve diğerleri
Baskı/Yayın Bilgisi: (2020-01-01)

Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
Yazar:: Mauricio Ayala-Rincón, ve diğerleri
Baskı/Yayın Bilgisi: (2013-01-01)

A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts
Yazar:: Zheng Yang, ve diğerleri
Baskı/Yayın Bilgisi: (2020-01-01)

Refinement modeling and verification of secure operating systems for communication in digital twins
Yazar:: Zhenjiang Qian, ve diğerleri
Baskı/Yayın Bilgisi: (2024-04-01)

Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions /
Yazar:: 183708 Bertot, Yves, ve diğerleri
Baskı/Yayın Bilgisi: (2004)

Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation
Yazar:: Haitao Wang, ve diğerleri
Baskı/Yayın Bilgisi: (2021-01-01)

Pengembangan Perangkat Pembelajaran Geometri Ruang dengan Model Proving Theorem
Yazar:: Bambang Eko Susilo, ve diğerleri
Baskı/Yayın Bilgisi: (2016-03-01)

FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq
Yazar:: Zheng Yang, ve diğerleri
Baskı/Yayın Bilgisi: (2019-01-01)

Another look at automated theorem-proving
Yazar:: Koblitz Neal
Baskı/Yayın Bilgisi: (2007-12-01)

Formal modeling and analyzing method for database security policy
Yazar:: Rong WANG, ve diğerleri
Baskı/Yayın Bilgisi: (2015-09-01)

Formal modeling and analyzing method for database security policy
Yazar:: Rong WANG, ve diğerleri
Baskı/Yayın Bilgisi: (2015-09-01)

A computational logic /
Yazar:: 403382 Boyer, Robert S., ve diğerleri
Baskı/Yayın Bilgisi: (1979)

HOW DOES PRE-SERVICE MATHEMATICS TEACHER PROVE THE LIMIT OF A FUNCTION BY FORMAL DEFINITION?
Yazar:: Rina Oktaviyanthi, ve diğerleri
Baskı/Yayın Bilgisi: (2018-06-01)

Research on formal security policy model specification and its formal analysis
Yazar:: LI Li-ping1, ve diğerleri
Baskı/Yayın Bilgisi: (2006-01-01)

Research on formal security policy model specification and its formal analysis
Yazar:: LI Li-ping1, ve diğerleri
Baskı/Yayın Bilgisi: (2006-01-01)

Another look at automated theorem-proving II
Yazar:: Koblitz Neal
Baskı/Yayın Bilgisi: (2012-02-01)

A survey of smart contract formal specification and verification
Yazar:: Tolmach, Palina, ve diğerleri
Baskı/Yayın Bilgisi: (2022)

State-of-the-art survey of smart contract verification based on formal methods
Yazar:: Wenbo ZHANG, ve diğerleri
Baskı/Yayın Bilgisi: (2022-08-01)

State-of-the-art survey of smart contract verification based on formal methods
Yazar:: Wenbo ZHANG, ve diğerleri
Baskı/Yayın Bilgisi: (2022-08-01)

Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
Yazar:: Ferruccio Guidi
Baskı/Yayın Bilgisi: (2012-01-01)

LoET-E: A Refined Theory for Proving Security Properties of Cryptographic Protocols
Yazar:: Jiawen Song, ve diğerleri
Baskı/Yayın Bilgisi: (2019-01-01)

SPECIFICATION FORMALIZATION OF STATE CHARTS FOR COMPLEX SYSTEM MANAGEMENT
Yazar:: Dmytro Nikitin
Baskı/Yayın Bilgisi: (2023-07-01)

Proving, Refuting, Improving—Looking for a Theorem
Yazar:: Branislav Boričić
Baskı/Yayın Bilgisi: (2022-10-01)

Automated Deduction -- CADE-21 [electronic resource] : 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings /
Yazar:: International Conference on Automated Deduction (21st : 2007 : Bremen, Germany), ve diğerleri
Baskı/Yayın Bilgisi: (2007)

Toward Secure and Reliable IoT Systems: A Comprehensive Review of Formal Methods Applications
Yazar:: Ikram Haddou-Oumouloud, ve diğerleri
Baskı/Yayın Bilgisi: (2024-01-01)

Modeling and verification of finite field multiplier using formal method
Yazar:: Zhang Jie, ve diğerleri
Baskı/Yayın Bilgisi: (2018-01-01)

Formal Verification of Blockchain Smart Contracts via ATL Model Checking
Yazar:: Wonhong Nam, ve diğerleri
Baskı/Yayın Bilgisi: (2022-01-01)

Didactical Transposition within Reflective Practice of an Indonesian Mathematics Teacher Community: A Case in Proving the Pythagorean Theorem Topic
Yazar:: Rudi Rudi, ve diğerleri
Baskı/Yayın Bilgisi: (2022-03-01)

A Novel Combinational ATP Based on Contradiction Separation for First-Order Logic
Yazar:: Jian Zhong, ve diğerleri
Baskı/Yayın Bilgisi: (2020-06-01)