| 2026 | TASE | Formal Verification of a Rust-Based Buddy Physical Memory Allocator. | Shaojie Wang, Yuting Wang, Qianying Zhang, Weituo Dai, Tian'ao Xie, Shijun Zhao, Yongwang Zhao |
| 2025 | SETTA | Strategy-Aware Liquidity for Account-Based Blockchains. | Ximeng Li, Sensen Chen, Yong Guan, Qianying Zhang, Guohui Wang, Zhi-Ping Shi |
| 2024 | FASE | Refinement Verification of OS Services based on a Verified Preemptive Microkernel. | Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang, Zhiping Shi |
| 2023 | APSEC | Formal Verification of Interrupt Isolation for the TrustZone-based TEE. | Leping Zhang, Qianying Zhang, Xinyue Wang, Ximeng Li, Guohui Wang, Zhiping Shi, Yong Guan |
| 2022 | QRS | Design and Implementation of OOM Module based on Rust. | Linhan Li, Qianying Zhang, Shijun Zhao, Zhi-Ping Shi, Yong Guan |
| 2021 | SETTA | Reasoning About Iteration and Recursion Uniformly Based on Big-Step Semantics. | Ximeng Li, Qianying Zhang, Guohui Wang, Zhiping Shi, Yong Guan |
| 2020 | APSEC | Formal Verification of Memory Isolation for the TrustZone-based TEE. | Yuwei Ma, Qianying Zhang, Shijun Zhao, Guohui Wang, Ximeng Li, Zhiping Shi |
| 2020 | ICFEM | Formalizing the Transaction Flow Process of Hyperledger Fabric. | Xiangyu Chen, Ximeng Li, Qianying Zhang, Zhiping Shi, Yong Guan |
| 2019 | APSEC | Formal Modelling and Verification of Spinlocks at Instruction Level. | Leping Zhang, Qianying Zhang, Guohui Wang, Zhiping Shi, Minhua Wu, Yong Guan |
| 2019 | CCS | SecTEE: A Software-based Approach to Secure Enclave Architecture Using TEE. | Shijun Zhao, Qianying Zhang, Yu Qin, Wei Feng, Dengguo Feng |
| 2019 | ICFEM | Towards Verifying Ethereum Smart Contracts at Intermediate Language Level. | Ximeng Li, Zhiping Shi, Qianying Zhang, Guohui Wang, Yong Guan, Ning Han |
| 2019 | RAID | Minimal Kernel: An Operating System Architecture for TEE to Resist Board Level Physical Attacks. | Shijun Zhao, Qianying Zhang, Yu Qin, Wei Feng, Dengguo Feng |
| 2019 | TrustCom | MicroTEE: Designing TEE OS Based on the Microkernel Architecture. | Dongxu Ji, Qianying Zhang, Shijun Zhao, Zhiping Shi, Yong Guan |
| 2018 | ICFEM | Formalization of Symplectic Geometry in HOL-Light. | Guohui Wang, Yong Guan, Zhiping Shi, Qianying Zhang, Xiaojuan Li, Yongdong Li |
| 2015 | ISPEC | sHMQV: An Efficient Key Exchange Protocol for Power-Limited Devices. | Shijun Zhao, Qianying Zhang |
| 2014 | CCS | Providing Root of Trust for ARM TrustZone using On-Chip SRAM. | Shijun Zhao, Qianying Zhang, Guangyao Hu, Yu Qin, Dengguo Feng |
| 2014 | ICICS | Mdaak: A Flexible and Efficient Framework for Direct Anonymous Attestation on Mobile Devices. | Qianying Zhang, Shijun Zhao, Li Xi, Wei Feng, Dengguo Feng |
| 2014 | NSS | Universally Composable Secure TNC Protocol Based on IF-T Binding to TLS. | Shijun Zhao, Qianying Zhang, Yu Qin, Dengguo Feng |
| 2014 | SecureComm | Improving the Security of the HMQV Protocol Using Tamper-Proof Hardware. | Qianying Zhang, Shijun Zhao, Yu Qin, Dengguo Feng |
| 2011 | TrustCom | A Property-Based Attestation Scheme with the Variable Privacy. | Yu Qin, Dexian Chang, Shijun Zhao, Qianying Zhang |