Explanipedia

The LLM Era Demands Natural-Language-Aligned Theorem Provers for Mathematics Open

Qinxiang Cao, Lihan Xie, Junchi Yan · 2025

Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic Open

Sheng-jia Wu, Xiwei Wu, Qinxiang Cao · 2025

Verifying a real-world program’s functional correctness can be decomposed into (1) a refinement proof showing that the program implements a more abstract high-level program and (2) an algorithm correctness proof at the high level. Relation…

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving Open

Qi Liu, Xinhao Zheng, Renqiu Xia, Xiangtong Qi, Qinxiang Cao , et al. · 2025

As a seemingly self-explanatory task, problem-solving has been a significant component of science and engineering. However, a general yet concrete formulation of problem-solving itself is missing. With the recent development of AI-based pr…

C*: Unifying Programming and Verification in C Open

Yiyuan Cao, Jingyi Zhuang, Han Chen, Jinkai Fan, Wenbo Xu , et al. · 2025

Ensuring the correct functionality of systems software, given its safety-critical and low-level nature, is a primary focus in formal verification research and applications. Despite advances in verification tooling, conventional programmers…

A Natural Formalized Proof Language Open

Lihan Xie, Zhicheng Hui, Qinxiang Cao · 2024

Artificial intelligence assisted mathematical proof has become a highly focused area nowadays. One key problem in this field is to generate formal mathematical proofs from natural language proofs. Due to historical reasons, the formal proo…

Denotation-based Compositional Compiler Verification Open

Zheng Cheng, Jiyang Wu, Di Wang, Qinxiang Cao · 2024

A desired but challenging property of compiler verification is compositionality in the sense that the compilation correctness of a program can be deduced from that of its substructures ranging from statements, functions, and modules increm…

A Coq Library of Sets for Teaching Denotational Semantics Open

Qinxiang Cao, Xiwei Wu, Yalun Liang · 2024

Sets and relations are very useful concepts for defining denotational\nsemantics. In the Coq proof assistant, curried functions to Prop are used to\nrepresent sets and relations, e.g. A -> Prop, A -> B -> Prop, A -> B -> C ->\nProp, etc. F…

VST-A: A Foundationally Sound Annotation Verifier Open

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

Program verifiers for imperative languages such as C may be annotation-based , in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are interactively dev…

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation Open

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

Program verification is vital for ensuring software reliability, especially in the context of increasingly complex systems. Loop invariants, remaining true before and after each iteration of loops, are crucial for this verification process…

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

Zhongye Wang, Qinxiang Cao, Yi‐Chen Tao · 2023

Many foundational program verification tools have been developed to build machine-checked program correctness proofs, a majority of which are based on Hoare logic. Their program logics, their assertion languages, and their underlying progr…

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

Zhongye Wang, Qinxiang Cao, Yi‐Chen Tao · 2023

Many foundational program verification tools have been developed to build machine-checkable program correctness proofs, a majority of which are based on Hoare logic. Their program logics, their assertion languages, and their underlying pro…

Coq Formalization of ZFC Set Theory for Teaching Scenarios Open

Xinyi Wan, Ke Xu, Qinxiang Cao · 2023

Multi-View Graph Representation for Programming Language Processing: An Investigation into Algorithm Detection Open

Ting Long, Yutong Xie, Xianyu Chen, Weinan Zhang, Qinxiang Cao , et al. · 2022

Program representation, which aims at converting program source code into vectors with automatically extracted features, is a fundamental problem in programming language processing (PLP). Recent work tries to represent programs with neural…

Multi-View Graph Representation for Programming Language Processing: An Investigation into Algorithm Detection Open

Ting Long, Yutong Xie, Xianyu Chen, Weinan Zhang, Qinxiang Cao , et al. · 2022

Program representation, which aims at converting program source code into vectors with automatically extracted features, is a fundamental problem in programming language processing (PLP). Recent work tries to represent programs with neural…

Symbolic Reasoning About Quantum Circuits in Coq Open

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

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

Qinxiang Cao, Xiwei Wu · 2021

The set of integer number lists with finite length, and the set of binary trees with integer labels are both countably infinite. Many inductively defined types also have countably many elements. In this paper, we formalize the syntax of fi…

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

Qinxiang Cao, Xiwei Wu · 2021

The set of integer number lists with finite length, and the set of binary\ntrees with integer labels are both countably infinite. Many inductively defined\ntypes also have countably many elements. In this paper, we formalize the syntax\nof…

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

Shengyi Wang, Qinxiang Cao, Anshuman Mohan, Aquinas Hobor · 2019

We develop powerful and general techniques to mechanically verify realistic programs that manipulate heap-represented graphs. These graphs can exhibit well-known organization principles, such as being a directed acyclic graph or a disjoint…

Proof Pearl: Magic Wand as Frame Open

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

Separation logic adds two connectives to assertion languages: separating conjunction * ("star") and its adjoint, separating implication -* ("magic wand"). Comparatively, separating implication is less widely used. This paper demonstrates t…

VST-A: A Foundationally Sound Annotation Verifier Open

Qinshi Wang, Qinxiang Cao · 2019

Program verifiers for imperative languages such as C may be annotation-based, in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are interactively deve…

Certifying Graph-Manipulating C Programs via Localizations within Data Structures Open

Shengyi Wang, Qinxiang Cao, Anshuman Mohan, Aquinas Hobor · 2019

We develop powerful and general techniques to mechanically verify realistic programs that manipulate heap- represented graphs. These graphs can exhibit well-known organization principles, such as being a directed acyclic graph or a disjoin…

Qinxiang Cao YOU? Author Swipe