Qinxiang Cao

44 papers A* 3B 1Misc 7Journal 30Unranked 2
YearRankTypeTitle / Venue / Authors
2026 J jnl
Denotation-based Compositional Compiler Verification.
ACM Trans. Program. Lang. Syst.
Zhang Cheng, Jiyang Wu, Di Wang, Qinxiang Cao
2026 J jnl
Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications.
CoRR
Liao Zhang, Tong Chen, Xiwei Wu, Qi Liu, Xiyu Zhai, Xinqi Wang, Qinxiang Cao
2025 Misc conf
A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms.
TASE
Chengxi Yang, Shushu Wu, Qinxiang Cao
2025 J jnl
A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms.
CoRR
Chengxi Yang, Shushu Wu, Qinxiang Cao
2025 J jnl
Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries.
CoRR
Fanpeng Yang, Xu Ma, Shuling Wang, Xiong Xu, Qinxiang Cao, Naijun Zhan, Xiaofeng Li, Bin Gu
2025 J jnl
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving.
CoRR
Qi Liu, Xinhao Zheng, Renqiu Xia, Xingzhi Qi, Qinxiang Cao, Junchi Yan
2025 J jnl
C*: Unifying Programming and Verification in C.
CoRR
Yiyuan Cao, Jiayi Zhuang, Houjin Chen, Jinkai Fan, Wenbo Xu, Zhiyi Wang, Di Wang, Qinxiang Cao, Yingfei Xiong, Haiyan Zhao, Zhenjiang Hu
2025 J jnl
Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic.
CoRR
Shushu Wu, Xiwei Wu, Qinxiang Cao
2025 J jnl
Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic.
Proc. ACM Program. Lang.
Shushu Wu, Xiwei Wu, Qinxiang Cao
2025 J jnl
Learning to Guarantee Type Correctness in Code Generation through Type-Guided Program Synthesis.
CoRR
Zhechong Huang, Zhao Zhang, Ruyi Ji, Tingxuan Xia, Qihao Zhu, Qinxiang Cao, Zeyu Sun, Yingfei Xiong
2025 J jnl
NEAT: QCP: A Practical Separation Logic-based C Program Verification Tool.
CoRR
Xiwei Wu, Yueyang Feng, Xiaoyang Lu, Tianchuan Lin, Kan Liu, Zhiyi Wang, Shushu Wu, Lihan Xie, Chengxi Yang, Hongyi Zhong, Naijun Zhan, Zhenjiang Hu, Qinxiang Cao
2025 A* conf
Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach.
ICLR
Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, Junchi Yan
2025 J jnl
Stellis: A Strategy Language for Purifying Separation Logic Entailments.
CoRR
Zhiyi Wang, Xiwei Wu, Yi Fang, Chengtao Li, Hongyi Zhong, Lihan Xie, Qinxiang Cao, Zhenjiang Hu
2025 Misc conf
VEP: A Two-stage Verification Toolchain for Full eBPF Programmability.
NSDI
Xiwei Wu, Yueyang Feng, Tianyi Huang, Xiaoyang Lu, Shengkai Lin, Lihan Xie, Shizhen Zhao, Qinxiang Cao
2024 Misc conf
A Natural Formalized Proof Language.
TASE
Lihan Xie, Zhicheng Hui, Qinxiang Cao
2024 J jnl
A Natural Formalized Proof Language.
CoRR
Lihan Xie, Zhicheng Hui, Qinxiang Cao
2024 J jnl
Denotation-based Compositional Compiler Verification.
CoRR
Zhang Cheng, Jiyang Wu, Di Wang, Qinxiang Cao
2024 Misc conf
Extending Symbolic Heap to Support Shared Ownership.
SETTA
Jiyang Wu, Qinxiang Cao
2024 J jnl
Formal Verification of Functional Correctness for Mutexes in Microkernel.
Int. J. Softw. Informatics
Linyan Zhang, Ximeng Li, Zhi-Ping Shi, Yong Guan, Qinxiang Cao, Qianying Zhang
2024 J jnl
Formalizing the Semantics of a Classical-Quantum Imperative Language in Coq.
J. Circuits Syst. Comput.
Wenjun Shi, Qinxiang Cao, Yuxin Deng
2024 J jnl
Preface to the Special Issue on Formal Methods and Applications.
Int. J. Softw. Informatics
Qinxiang Cao, Fu Song, Naijun Zhan
2024 A* conf
Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation.
NeurIPS
Chang Liu, Xiwei Wu, Yuan Feng, Qinxiang Cao, Junchi Yan
2024 J jnl
VST-A: A Foundationally Sound Annotation Verifier.
Proc. ACM Program. Lang.
Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao
2024 J jnl
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding.
J. Autom. Reason.
Zhongye Wang, Qinxiang Cao, Yichen Tao
2023 — conf
A Coq Library of Sets for Teaching Denotational Semantics.
ThEdu@CADE
Qinxiang Cao, Xiwei Wu, Yalun Liang
2023 J jnl
Coq Formalization of ZFC Set Theory for Teaching Scenarios.
Int. J. Softw. Informatics
Xinyi Wan, Ke Xu, Qinxiang Cao
2023 Misc conf
Formalization of Lambda Calculus with Explicit Names as a Nominal Reasoning Framework.
SETTA
Xinyi Wan, Qinxiang Cao
2023 J jnl
Towards General Loop Invariant Generation via Coordinating Symbolic Execution and Large Language Models.
CoRR
Chang Liu, Xiwei Wu, Yuan Feng, Qinxiang Cao, Junchi Yan
2023 J jnl
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding v.s. Shallow Embedding.
CoRR
Zhongye Wang, Qinxiang Cao, Yichen Tao
2022 Misc conf
LOGIC: A Coq Library for Logics.
SETTA
Yichen Tao, Qinxiang Cao
2022 A* conf
Multi-View Graph Representation for Programming Language Processing: An Investigation into Algorithm Detection.
AAAI
Ting Long, Yutong Xie, Xianyu Chen, Weinan Zhang, Qinxiang Cao, Yong Yu
2022 J jnl
Multi-View Graph Representation for Programming Language Processing: An Investigation into Algorithm Detection.
CoRR
Ting Long, Yutong Xie, Xianyu Chen, Weinan Zhang, Qinxiang Cao, Yong Yu
2021 — conf
Countability of Inductive Types Formalized in the Object-Logic Level.
LFMTP
Qinxiang Cao, Xiwei Wu
2021 J jnl
Resisting newborn attacks via shared Proof-of-Space.
J. Parallel Distributed Comput.
Shuyang Tang, Jilai Zheng, Yao Deng, Qinxiang Cao
2021 J jnl
Symbolic Reasoning About Quantum Circuits in Coq.
J. Comput. Sci. Technol.
Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng
2020 Misc conf
Reentrancy? Yes. Reentrancy Bug? No.
SETTA
Qinxiang Cao, Zhongye Wang
2020 J jnl
Symbolic Reasoning about Quantum Circuits in Coq.
CoRR
Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng
2019 J jnl
Certifying graph-manipulating C programs via localizations within data structures.
Proc. ACM Program. Lang.
Shengyi Wang, Qinxiang Cao, Anshuman Mohan, Aquinas Hobor
2019 J jnl
Proof Pearl: Magic Wand as Frame.
CoRR
Qinxiang Cao, Shengyi Wang, Aquinas Hobor, Andrew W. Appel
2019 J jnl
VST-A: A Foundationally Sound Annotation Verifier.
CoRR
Qinshi Wang, Qinxiang Cao
2018 — —
Separation-Logic-Based Program Verification in Coq
Qinxiang Cao
2018 J jnl
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs.
J. Autom. Reason.
Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel
2017 B conf
Bringing Order to the Separation Logic Jungle.
APLAS
Qinxiang Cao, Santiago Cuéllar, Andrew W. Appel
2013 J jnl
On axiomatizations of public announcement logic.
Synth.
Yanjing Wang, Qinxiang Cao