39 citations · 84 across the 7 of their papers we have counts for
7 papers
DPCP-p: A Distributed Locking Protocol for Parallel Real-Time Tasks
Maolin Yang, Zewei Chen, Xu Jiang +2
Real-time scheduling and locking protocols are fundamental facilities to construct time-critical systems. For parallel real-time tasks, predictable locking protocols are required w…
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts
Zheng Yang, Hang Lei, Weizhong Qian
This paper reports on the development of a formal symbolic process virtual machine (FSPVM) denoted as FSPVM-E for verifying the reliability and security of Ethereum-based services…
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…