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...
Auteurs principaux: | Zheng Yang, Hang Lei |
---|---|
Format: | Article |
Langue: | English |
Publié: |
IEEE
2018-01-01
|
Collection: | IEEE Access |
Sujets: | |
Accès en ligne: | https://ieeexplore.ieee.org/document/8531607/ |
Documents similaires
-
Symbolic logic and mechanical theorem proving /
par: 336504 Chang, Chin-Ling, et autres
Publié: (1973) -
Formal analysis of 2D image processing filters using higher-order logic theorem proving
par: Adnan Rashid, et autres
Publié: (2022-06-01) -
Formal Verification of Fractional-Order PID Control Systems Using Higher-Order Logic
par: Chunna Zhao, et autres
Publié: (2022-08-01) -
Logic for computer science : foundations of automatic theorem proving /
par: 455116 Gallier, Jean H.
Publié: (1986) -
Formal verification of Matrix based MATLAB models using interactive theorem proving
par: Ayesha Gauhar, et autres
Publié: (2021-03-01)