Towards Verifying Ethereum Smart Contracts at Intermediate Language Level. - Ximeng Li 003; Zhiping Shi 002; Qianying Zhang; Guohui Wang; Yong Guan; Ning Han (ICFEM, 2019)

A HOL Theory of the Differential for Matrix Functions. - Yuhan Nie; Zhiping Shi 002; Aixuan Wu; Ximeng Li 003; Guohui Wang; Yong Guan (TASE, 2019)

Formal Verification of Atomicity Requirements for Smart Contracts. - Ning Han; Ximeng Li 003; Guohui Wang; Zhiping Shi 002; Yong Guan (APLAS, 2020)

Formal Verification of Memory Isolation for the TrustZone-based TEE. - Yuwei Ma; Qianying Zhang; Shijun Zhao; Guohui Wang; Ximeng Li 003; Zhiping Shi 002 (APSEC, 2020)

Formalizing the Transaction Flow Process of Hyperledger Fabric. - Xiangyu Chen; Ximeng Li 003; Qianying Zhang; Zhiping Shi 002; Yong Guan (ICFEM, 2020)

Formalization of Camera Pose Estimation Algorithm based on Rodrigues Formula. - Shanyan Chen; Guohui Wang; Ximeng Li 003; Qianying Zhang; Zhi-Ping Shi 002; Yong Guan (Formal Aspects Comput., 2020)

Reasoning About Iteration and Recursion Uniformly Based on Big-Step Semantics. - Ximeng Li 003; Qianying Zhang; Guohui Wang; Zhiping Shi 002; Yong Guan (SETTA, 2021)

Formalization of Euler-Lagrange Equation Set Based on Variational Calculus in HOL Light. - Yong Guan; Jingzhi Zhang; Guohui Wang; Ximeng Li 003; Zhiping Shi 002; Yongdong Li (J. Autom. Reason., 2021)

Formal Verification of Interrupt Isolation for the TrustZone-based TEE. - Leping Zhang; Qianying Zhang; Xinyue Wang; Ximeng Li 003; Guohui Wang; Zhiping Shi 002; Yong Guan (APSEC, 2023)

Formalization of Robot Collision Detection Method based on Conformal Geometric Algebra. - Yingjie Wu; Guohui Wang; Shanyan Chen; Zhiping Shi 002; Yong Guan; Ximeng Li 003 (CoRR, 2023)

A unified proof technique for verifying program correctness with big-step semantics. - Ximeng Li 003; Qianying Zhang; Guohui Wang; Zhi-Ping Shi 002; Yong Guan (J. Syst. Archit., 2023)

Formalization of the inverse kinematics of three-fingered dexterous hand. - Guohui Wang; Shanyan Chen; Yong Guan; Zhi-Ping Shi 002; Ximeng Li 003; Jingzhi Zhang (J. Log. Algebraic Methods Program., 2023)

Refinement Verification of OS Services based on a Verified Preemptive Microkernel. - Ximeng Li 003; Shanyan Chen; Yong Guan; Qianying Zhang; Guohui Wang; Zhiping Shi 002 (FASE, 2024)

Formal Verification of Functional Correctness for Mutexes in Microkernel. - Linyan Zhang; Ximeng Li 003; Zhi-Ping Shi 002; Yong Guan; Qinxiang Cao; Qianying Zhang (Int. J. Softw. Informatics, 2024)