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
Предметы:
Online-ссылка:https://ieeexplore.ieee.org/document/8531607/