39 citations · 84 across the 7 of their papers we have counts for
5 papers · 1 filter
FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq
Zheng Yang, Hang Lei
Blockchain technology adds records to a list using cryptographic links. Therefore, the security of blockchain smart contracts is among the most popular contemporary research topics…
Optimization of Executable Formal Interpreters developed in Higher-order Theorem Proving Systems
Zheng Yang, Hang Lei
In recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order theorem proving and symbolic execution for verifyi…
Formal Process Virtual Machine for Smart Contracts Verification
Zheng Yang, Hang Lei
This paper reports on the development and verification of a novel formal symbolic process virtual machine (FSPVM) for verifying the reliability and security of Ethereum smart contr…
A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability
Zheng Yang, Hang Lei
In recent years, a number of lightweight programs have been deployed in critical domains, such as in smart contracts based on blockchain technology. Therefore, the security and rel…
Lolisa: Formal syntax and semantics for a subset of the solidity programming language in Mathematical Tool Coq
Zheng Yang, Hang Lei
This article presents the formal syntax and semantics for a large subset of the Solidity programming language developed for the Etheruem blockchain platform based on our resent wor…