Qinxiang Cao

According to our database, Qinxiang Cao authored at least 24 papers between 2013 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding.

Zhongye Wang, Qinxiang Cao, Yichen Tao

J. Autom. Reason., September, 2024

Formalizing the Semantics of a Classical-Quantum Imperative Language in Coq.

Wenjun Shi, Qinxiang Cao, Yuxin Deng

J. Circuits Syst. Comput., April, 2024

VST-A: A Foundationally Sound Annotation Verifier.

Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao

Proc. ACM Program. Lang., January, 2024

Denotation-based Compositional Compiler Verification.

Zhang Cheng, Jiyang Wu, Di Wang, Qinxiang Cao

CoRR, 2024

A Natural Formalized Proof Language.

Lihan Xie, Zhicheng Hui, Qinxiang Cao

Proceedings of the Theoretical Aspects of Software Engineering, 2024

Extending Symbolic Heap to Support Shared Ownership.

Jiyang Wu, Qinxiang Cao

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2024

2023

Coq Formalization of ZFC Set Theory for Teaching Scenarios.

Xinyi Wan, Ke Xu, Qinxiang Cao

Int. J. Softw. Informatics, 2023

A Coq Library of Sets for Teaching Denotational Semantics.

Qinxiang Cao, Xiwei Wu, Yalun Liang

Proceedings of the Proceedings 12th International Workshop on Theorem proving components for Educational software, 2023

Towards General Loop Invariant Generation via Coordinating Symbolic Execution and Large Language Models.

Chang Liu, Xiwei Wu, Yuan Feng, Qinxiang Cao, Junchi Yan

CoRR, 2023

Verifying Programs with Logic and Extended Proof Rules: Deep Embedding v.s. Shallow Embedding.

Zhongye Wang, Qinxiang Cao, Yichen Tao

CoRR, 2023

Formalization of Lambda Calculus with Explicit Names as a Nominal Reasoning Framework.

Xinyi Wan, Qinxiang Cao

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2023

2022

LOGIC: A Coq Library for Logics.

Yichen Tao, Qinxiang Cao

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2022

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

Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence, 2022

2021

Resisting newborn attacks via shared Proof-of-Space.

Shuyang Tang, Jilai Zheng, Yao Deng, Qinxiang Cao

J. Parallel Distributed Comput., 2021

Symbolic Reasoning About Quantum Circuits in Coq.

Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng

J. Comput. Sci. Technol., 2021

Countability of Inductive Types Formalized in the Object-Logic Level.

Qinxiang Cao, Xiwei Wu

Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2021

2020

Reentrancy? Yes. Reentrancy Bug? No.

Qinxiang Cao, Zhongye Wang

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2020

2019

Certifying graph-manipulating C programs via localizations within data structures.

Shengyi Wang, Qinxiang Cao, Anshuman Mohan, Aquinas Hobor

Proc. ACM Program. Lang., 2019

Proof Pearl: Magic Wand as Frame.

Qinxiang Cao, Shengyi Wang, Aquinas Hobor, Andrew W. Appel

CoRR, 2019

VST-A: A Foundationally Sound Annotation Verifier.

Qinshi Wang, Qinxiang Cao

CoRR, 2019

2018

Separation-Logic-Based Program Verification in Coq

Qinxiang Cao

PhD thesis, 2018

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

2017

Bringing Order to the Separation Logic Jungle.

Qinxiang Cao, Santiago Cuéllar, Andrew W. Appel

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2013

On axiomatizations of public announcement logic.

Yanjing Wang, Qinxiang Cao

Synth., 2013