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...
Autores principales: | Zheng Yang, Hang Lei |
---|---|
Formato: | Artículo |
Lenguaje: | English |
Publicado: |
IEEE
2018-01-01
|
Colección: | IEEE Access |
Materias: | |
Acceso en línea: | https://ieeexplore.ieee.org/document/8531607/ |
Ejemplares similares
-
Symbolic logic and mechanical theorem proving /
por: 336504 Chang, Chin-Ling, et al.
Publicado: (1973) -
Formal analysis of 2D image processing filters using higher-order logic theorem proving
por: Adnan Rashid, et al.
Publicado: (2022-06-01) -
Formal Verification of Fractional-Order PID Control Systems Using Higher-Order Logic
por: Chunna Zhao, et al.
Publicado: (2022-08-01) -
Logic for computer science : foundations of automatic theorem proving /
por: 455116 Gallier, Jean H.
Publicado: (1986) -
Formal verification of Matrix based MATLAB models using interactive theorem proving
por: Ayesha Gauhar, et al.
Publicado: (2021-03-01)