Author name cluster

Qinxiang Cao

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

FM Conference 2026 Conference Paper

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

Abstract OpenHarmony LiteOS-M, a preemptive operating system (OS) kernel for the Internet of Things (IoT), is widely deployed in safety-critical domains, such as aerospace and transportation. As a rigorous method to assure software safety, formal verification has been applied to OS kernels in industry. However, entirely verified kernels with large codebases are rare, since such verification is typically performed within interactive theorem provers, requiring substantial human effort. In this paper, we present the functional correctness verification of LiteOS-M. First, to improve verification efficiency, we design a formal verification platform, Smart Verifier. The platform employs an annotation-based verifier as the front end, while the back end integrates Z3 and Rocq, combining automatic and interactive theorem proving techniques. Second, we tailor two verification methods, expressing program refinement as standard Hoare logic triples and modeling concurrency through state transition systems, to utilize the platform for verifying LiteOS-M. Our verified LiteOS-M kernel consists of 17, 000 lines of C. During the code review and verification, we find a total of 17 bugs, all confirmed and fixed by developers.

DOI

NeurIPS Conference 2025 Conference Paper

Bootstrapping Hierarchical Autoregressive Formal Reasoner with Chain-of-Proxy-Autoformalization

Qi Liu
Xinhao Zheng
Renqiu Xia
Qinxiang Cao
Junchi Yan

Deductive formal problem-solving (D-FPS) enables process-verified, human-aligned problem-solving by implementing deductive solving processes within formal theorem proving (FTP) environments. However, current methods fail to address the misalignment between informal and formal reasoning granularity and suffer from inefficiency due to backtracking and error propagation. Moreover, the extreme scarcity of formal problem-solution pairs further hinders progress. For the first gap, we propose **HAR** (_**H**ierarchical **A**utoregressive Formal **R**easoner_), a novel reasoning pipeline. HAR decouples informal-aligned drafting and detailed proving, and formulates solution construction as autoregressive generation with per-step feedback. Second, we propose **CoPA** (_**C**hain-**o**f-**P**roxy-**A**utoformalization_), a data generation pipeline that cascades statement autoformalization, proof drafting, and proof search as a proxy autoformalization path. Experiments demonstrate significant improvements: trained on data bootstrapped by CoPA, HAR achieves superior performance on FormalMath500 ($15. 50\\%\mapsto 44. 09\\%$) and MiniF2F-Solving ($21. 87\\%\mapsto 56. 58\\%$) with lower computational budget. Explorations reveal promising directions in formal solution pruning and informal dataset denoising.

PDF Details

ICLR Conference 2025 Conference Paper

Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach

Qi Liu
Xinhao Zheng
Xudong Lu
Qinxiang Cao
Junchi Yan

As a central component in formal verification, statement autoformalization has been widely studied including the recent efforts from machine learning community, but still remains a widely-recognized difficult and open problem. In this paper, we delve into two critical yet under-explored gaps: 1) absence of faithful and universal automated evaluation for autoformalization results; 2) agnosia of contextual information, inducing severe hallucination of formal definitions and theorems. To address the first issue, we propose **BEq** (_**B**idirectional **E**xtended Definitional E**q**uivalence_), an automated neuro-symbolic method to determine the equivalence between two formal statements, which is formal-grounded and well-aligned with human intuition. For the second, we propose **RAutoformalizer** (_**R**etrieval-augmented **Autoformalizer**_), augmenting statement autoformalization by _Dependency Retrieval_, retrieving potentially dependent objects from formal libraries. We parse the dependencies of libraries and propose to _structurally informalise_ formal objects by the topological order of dependencies. To evaluate OOD generalization and research-level capabilities, we build a novel benchmark, _Con-NF_, consisting of 961 informal-formal statement pairs from frontier mathematical researches. Experiments validate the effectiveness of our approaches: BEq is evaluated on 200 diverse formal statement pairs with expert-annotated equivalence label, exhibiting significantly improved accuracy ($82.50\\% \mapsto 90.50\\%$) and precision ($70.59\\% \mapsto 100.0\\%$). For dependency retrieval, a strong baseline is devised. Our RAutoformalizer substantially outperforms SOTA baselines in both in-distribution ProofNet benchmark ($12.83\\% \mapsto 18.18\\%$, BEq@8) and OOD Con-NF scenario ($4.58\\%\mapsto 16.86\\%$, BEq@8).

Details

NeurIPS Conference 2024 Conference Paper

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

Chang Liu
Xiwei Wu
Yuan Feng
Qinxiang Cao
Junchi Yan

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. Traditional provers and machine learning based methods for generating loop invariants often require expert intervention or extensive labeled data, and typically only handle numerical property verification. These methods struggle with programs involving complex data structures and memory manipulations, limiting their applicability and automation capabilities. This paper introduces a new benchmark named LIG-MM, specifically for programs with complex data structures and memory manipulations. We collect 312 programs from various sources, including daily programs from college homework, the international competition (SV-COMP), benchmarks from previous papers (SLING), and programs from real-world software systems (Linux Kernel, GlibC, LiteOS, and Zephyr). Based on LIG-MM, our findings indicate that previous methods, including GPT-4, fail to automate verification for these programs. Consequently, we propose a novel LLM-SE framework that coordinates LLM with symbolic execution, fine-tuned using self-supervised learning, to generate loop invariants. Experimental results on LIG-MM demonstrate that our LLM-SE outperforms state-of-the-art methods, offering a new direction toward automated program verification in real-world scenarios.

PDF Details DOI

AAAI Conference 2022 Conference Paper

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

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 networks based on source code structures. However, such methods often focus on the syntax and consider only one single perspective of programs, limiting the representation power of models. This paper proposes a multiview graph (MVG) program representation method. MVG pays more attention to code semantics and simultaneously includes both data flow and control flow as multiple views. These views are then combined and processed by a graph neural network (GNN) to obtain a comprehensive program representation that covers various aspects. We thoroughly evaluate our proposed MVG approach in the context of algorithm detection, an important and challenging subfield of PLP. Specifically, we use a public dataset POJ-104 and also construct a new challenging dataset ALG-109 to test our method. In experiments, MVG outperforms previous methods significantly, demonstrating our model’s strong capability of representing source code.

PDF Details

LFMTP Workshop 2021 Workshop Paper

Countability of Inductive Types Formalized in the Object-Logic Level

Qinxiang Cao
Xiwei Wu

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 first order inductive definitions in Coq and prove them countable, under some side conditions. Instead of writing a proof generator in a meta language, we develop an axiom-free proof in the Coq object logic. In other words, our proof is a dependently typed Coq function from the syntax of the inductive definition to the countability of the type. Based on this proof, we provide a Coq tactic to automatically prove the countability of concrete inductive types. We also developed Coq libraries for countability and for the syntax of inductive definitions, which have value on their own.

Details DOI