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 |
Предмети: | |
Онлайн доступ: | 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)