Formal Verification of GP Specification based Embedded Operating System. - Haiyong Sun; Hang Lei; Lei Qiao; Zheng Yang 007 (CSAE, 2018)

Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems. - Zheng Yang 007; Hang Lei (IEEE Access, 2018)

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 007; Hang Lei (CoRR, 2018)

Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language. - Zheng Yang 007; Hang Lei (CoRR, 2018)

Formal Process Virtual Machine for Smart Contracts Verification. - Zheng Yang 007; Hang Lei (CoRR, 2018)

Optimization of Executable Formal Interpreters developed in Higher-order Theorem Proving Systems. - Zheng Yang 007; Hang Lei (CoRR, 2018)

FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq. - Zheng Yang 007; Hang Lei (IEEE Access, 2019)

A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts. - Zheng Yang 007; Hang Lei; Weizong Qian (CoRR, 2019)

A Resolution for Scalability Problem of Record Datatype Based Formal Memory Models in Coq. - Zheng Yang 007; Hang Lei; Weizhong Qian; Zehui Yan; Weiru Zeng (CSAE, 2020)

A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts. - Zheng Yang 007; Hang Lei; Weizhong Qian (IEEE Access, 2020)

Formal Verification Platform as a Service: WebAssembly Vulnerability Detection Application. - Liangjun Deng; Hang Lei; Zheng Yang 007; Weizhong Qian; Xiaoyu Li; Hao Wu; Sihao Deng; Ruchao Sha; Weidong Deng (Comput. Syst. Sci. Eng., 2023)