On axiomatizations of public announcement logic. - Yanjing Wang 001; Qinxiang Cao (Synth., 2013)

Bringing Order to the Separation Logic Jungle. - Qinxiang Cao; Santiago Cuéllar; Andrew W. Appel (APLAS, 2017)

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. - Qinxiang Cao; Lennart Beringer; Samuel Gruetter; Josiah Dodds; Andrew W. Appel (J. Autom. Reason., 2018)

Separation-Logic-Based Program Verification in Coq - Qinxiang Cao (2018)

VST-A: A Foundationally Sound Annotation Verifier. - Qinshi Wang; Qinxiang Cao (CoRR, 2019)

Proof Pearl: Magic Wand as Frame. - Qinxiang Cao; Shengyi Wang; Aquinas Hobor; Andrew W. Appel (CoRR, 2019)

Certifying graph-manipulating C programs via localizations within data structures. - Shengyi Wang; Qinxiang Cao; Anshuman Mohan; Aquinas Hobor (Proc. ACM Program. Lang., 2019)

Reentrancy? Yes. Reentrancy Bug? No. - Qinxiang Cao; Zhongye Wang (SETTA, 2020)

Countability of Inductive Types Formalized in the Object-Logic Level. - Qinxiang Cao; Xiwei Wu (LFMTP, 2021)

Symbolic Reasoning About Quantum Circuits in Coq. - Wenjun Shi; Qinxiang Cao; Yuxin Deng; Hanru Jiang; Yuan Feng 001 (J. Comput. Sci. Technol., 2021)

Resisting newborn attacks via shared Proof-of-Space. - Shuyang Tang; Jilai Zheng; Yao Deng; Qinxiang Cao (J. Parallel Distributed Comput., 2021)

Multi-View Graph Representation for Programming Language Processing: An Investigation into Algorithm Detection. - Ting Long; Yutong Xie 007; Xianyu Chen; Weinan Zhang 001; Qinxiang Cao; Yong Yu 001 (AAAI, 2022)

LOGIC: A Coq Library for Logics. - Yichen Tao; Qinxiang Cao (SETTA, 2022)

Formalization of Lambda Calculus with Explicit Names as a Nominal Reasoning Framework. - Xinyi Wan; Qinxiang Cao (SETTA, 2023)

Verifying Programs with Logic and Extended Proof Rules: Deep Embedding v.s. Shallow Embedding. - Zhongye Wang; Qinxiang Cao; Yichen Tao (CoRR, 2023)

Towards General Loop Invariant Generation via Coordinating Symbolic Execution and Large Language Models. - Chang Liu 021; Xiwei Wu; Yuan Feng 001; Qinxiang Cao; Junchi Yan (CoRR, 2023)

A Coq Library of Sets for Teaching Denotational Semantics. - Qinxiang Cao; Xiwei Wu; Yalun Liang (ThEdu@CADE, 2023)

Coq Formalization of ZFC Set Theory for Teaching Scenarios. - Xinyi Wan; Ke Xu; Qinxiang Cao (Int. J. Softw. Informatics, 2023)

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation. - Chang Liu 021; Xiwei Wu; Yuan Feng 001; Qinxiang Cao; Junchi Yan (NeurIPS, 2024)

Extending Symbolic Heap to Support Shared Ownership. - Jiyang Wu; Qinxiang Cao (SETTA, 2024)

A Natural Formalized Proof Language. - Lihan Xie; Zhicheng Hui; Qinxiang Cao (TASE, 2024)

Denotation-based Compositional Compiler Verification. - Zhang Cheng; Jiyang Wu; Di Wang; Qinxiang Cao (CoRR, 2024)

Preface to the Special Issue on Formal Methods and Applications. - Qinxiang Cao; Fu Song; Naijun Zhan (Int. J. Softw. Informatics, 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)

VST-A: A Foundationally Sound Annotation Verifier. - Litao Zhou; Jianxing Qin; Qinshi Wang; Andrew W. Appel; Qinxiang Cao (Proc. ACM Program. Lang., 2024)

Formalizing the Semantics of a Classical-Quantum Imperative Language in Coq. - Wenjun Shi; Qinxiang Cao; Yuxin Deng (J. Circuits Syst. Comput., 2024)

Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding. - Zhongye Wang; Qinxiang Cao; Yichen Tao (J. Autom. Reason., 2024)

Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach. - Qi Liu; Xinhao Zheng; Xudong Lu; Qinxiang Cao; Junchi Yan (ICLR, 2025)

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 (NSDI, 2025)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms. - Chengxi Yang; Shushu Wu; Qinxiang Cao (TASE, 2025)

C*: Unifying Programming and Verification in C. - Yiyuan Cao; Jiayi Zhuang; Houjin Chen; Jinkai Fan; Wenbo Xu; Zhiyi Wang; Di Wang 017; Qinxiang Cao; Yingfei Xiong 001; Haiyan Zhao 001; Zhenjiang Hu (CoRR, 2025)

Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic. - Shushu WU; Xiwei WU; Qinxiang Cao (CoRR, 2025)

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving. - Qi Liu; Xinhao Zheng; Renqiu Xia; Xingzhi Qi; Qinxiang Cao; Junchi Yan (CoRR, 2025)

NEAT: 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; Naijun Zhan; Zhenjiang Hu; et al. (CoRR, 2025)

Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries. - Fanpeng Yang; Xu Ma; Shuling Wang 003; Xiong Xu; Qinxiang Cao; Naijun Zhan; Xiaofeng Li; Bin Gu 006 (CoRR, 2025)