| 2026 | FM | Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel. | Tianqi Zhao, Qinxiang Cao, Shenghua Feng, Minghui Zhou, Naijun Zhan, Yongzhi Cao, Junfeng Zhao, Haiyan Zhao, Hao Wang, Zhenjiang Hu |
| 2026 | TASE | QCP: A Practical Separation Logic-Based C Program Verification Tool. | Xiwei Wu, Yueyang Feng, Xiaoyang Lu, Tianchuan Lin, Kan Liu, Zhiyi Wang, Shushu Wu, Lihan Xie, Chengxi Yang, Hongyi Zhong, Zihan Zhang, Juanru Li, Naijun Zhan, Zhenjiang Hu, Qinxiang Cao |
| 2026 | TASE | Intuitive Verification of Sequential Programs Using Hybrid Reasoning. | Shushu Wu, Xiwei Wu, Chengxi Yang, Qinxiang Cao |
| 2025 | ICLR | Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach. | Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, Junchi Yan |
| 2025 | NSDI | VEP: A Two-stage Verification Toolchain for Full eBPF Programmability. | Xiwei Wu, Yueyang Feng, Tianyi Huang, Xiaoyang Lu, Shengkai Lin, Lihan Xie, Shizhen Zhao, Qinxiang Cao |
| 2025 | TASE | A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms. | Chengxi Yang, Shushu Wu, Qinxiang Cao |
| 2024 | SETTA | Extending Symbolic Heap to Support Shared Ownership. | Jiyang Wu, Qinxiang Cao |
| 2024 | TASE | A Natural Formalized Proof Language. | Lihan Xie, Zhicheng Hui, Qinxiang Cao |
| 2023 | SETTA | Formalization of Lambda Calculus with Explicit Names as a Nominal Reasoning Framework. | Xinyi Wan, Qinxiang Cao |
| 2022 | AAAI | Multi-View Graph Representation for Programming Language Processing: An Investigation into Algorithm Detection. | Ting Long, Yutong Xie, Xianyu Chen, Weinan Zhang, Qinxiang Cao, Yong Yu |
| 2022 | SETTA | LOGIC: A Coq Library for Logics. | Yichen Tao, Qinxiang Cao |
| 2020 | SETTA | Reentrancy? Yes. Reentrancy Bug? No. | Qinxiang Cao, Zhongye Wang |
| 2017 | APLAS | Bringing Order to the Separation Logic Jungle. | Qinxiang Cao, Santiago Cullar, Andrew W. Appel |