pith. sign in

arxiv: 2505.12878 · v3 · submitted 2025-05-19 · 💻 cs.PL · cs.SE

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
show 7 more authors
Chengxi Yang Hongyi Zhong Zihan Zhang Juanru Li Naijun Zhan Zhenjiang Hu Qinxiang Cao
This is my paper

Pith reviewed 2026-05-22 14:52 UTC · model grok-4.3

classification 💻 cs.PL cs.SE
keywords C program verificationseparation logicsymbolic executionRocqinteractive provingannotation-based verificationVS Code extensionformal verification
0
0 comments X

The pith

QCP combines automatic symbolic execution with Rocq interactive proofs to verify complex C programs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents QCP as a tool that lets developers add annotations to C code and then automatically checks many correctness properties using symbolic execution paired with a separation logic solver. When those automatic steps cannot finish the job, the remaining obligations are handed off for manual proof inside Rocq. The same system ships with a VS Code extension that helps users write the annotations, inspect what the solver has done, and complete the proofs. A reader would care because existing automatic tools often fail on realistic code while fully manual proof is too slow for large systems; QCP tries to split the difference so that most of the work stays automatic.

Core claim

QCP integrates annotation-based automatic verification with interactive proving using Rocq. It employs symbolic execution and a separation logic entailment solver to automatically discharge many verification obligations, while deferring more complex obligations to Rocq for manual proof. Furthermore, QCP includes a VS Code extension designed to enhance proof efficiency and support a deeper understanding of both the program behavior and verification outcomes.

What carries the argument

Hybrid pipeline that runs symbolic execution plus a separation logic entailment solver for automatic discharge and passes the rest to Rocq for interactive proof.

Load-bearing premise

Symbolic execution combined with a separation logic entailment solver will successfully discharge a large fraction of verification obligations in practice, leaving only manageable obligations for Rocq.

What would settle it

Applying QCP to several substantial real-world C codebases and finding that most obligations still require full manual Rocq proofs rather than being discharged automatically would show the automation does not scale as claimed.

Figures

Figures reproduced from arXiv: 2505.12878 by Chengxi Yang, Hongyi Zhong, Juanru Li, Kan Liu, Lihan Xie, Naijun Zhan, Qinxiang Cao, Shushu Wu, Tianchuan Lin, Xiaoyang Lu, Xiwei Wu, Yueyang Feng, Zhenjiang Hu, Zhiyi Wang, Zihan Zhang.

Figure 1
Figure 1. Figure 1: The components of QCP. QCP takes annotated C code as input and generates verification conditions. The straightforward conditions are discharged automatically, as shown in [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: example of sll_free. The predicate listrep describes the structural properties of singly-linked lists. In practical software verification, it is often necessary to reason about func￾tions at different levels of abstraction. A function may be equipped with both a concrete, implementation-oriented specification and more abstract specifica￾tions that capture its high-level behavior. To handle this, QCP mandat… view at source ↗
Figure 3
Figure 3. Figure 3: Specification of LOS_ListAdd and LOS_ListTailInsert from LiteOS. The predicate store_dll(x) represents a circular doubly-linked list storage structure, where x denotes the sentinel node. For example, [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The definition of LOS_DL_LIST in LiteOS. The node x serves as a sentinel node, and its pstData field remains unused. In this case, the LOS_ListAdd function is equipped with two specifications. The primitive_spec is used for the verification of LOS_ListAdd itself as well as the LOS_ListTailInsert function. Meanwhile, since LOS_ListAdd can also function as a routine for inserting a node at the head, an addit… view at source ↗
Figure 5
Figure 5. Figure 5: Live verification during code editing in VS Code. As for failure scenarios, [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Failure case for live verification during code editing in VS Code. For those cases that pass symbolic execution but cannot be fully solved au￾tomatically, we use yellow highlighting to distinguish them from failure cases. The corresponding code lines will be marked in yellow. In summary, QCP features an integrated development interface that provides immediate visual feedback during the verification process… view at source ↗
Figure 7
Figure 7. Figure 7: Example illustrating symbolic state during partial program execution, with different types of partial statements distinguished by color. Partial Statement ps ::= s singleton statement | asrt annotation statement | break | continue control-flow statement | return | return e return statement | if (e) | else conditional-if/else | switch(e) | case e: | default: switch-case-default | while (e) | do | for(s;e;s)… view at source ↗
Figure 8
Figure 8. Figure 8: Syntax of C partial statements. Singleton statements encompass assignments, increment/decrement operations, and function calls. The symbolic execution over partial statements follows conventional method￾ologies. During execution, QCP maintains a symbolic state stack [PITH_FULL_IMAGE:figures/full_fig_p009_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Syntax of Stellis P rog consists of a sequence of strategies S. A strategy S has the following four elements: 1. A priority r, specified using the priority label. 2. A sequence of patterns q. 3. A sequence of checks c, denoted by the check label. 4. An action a, indicated by the action label. The pattern part is used to identify specific formulas on both sides of the entailment. For right patterns, a patte… view at source ↗
Figure 10
Figure 10. Figure 10: The real verification file of sll_free. Regarding proof checking, we leverage Rocq’s Module Type mechanism. In sll_free_goal.v, we generate a Module Type named VC_Correct that con￾tains all verification goals (see [PITH_FULL_IMAGE:figures/full_fig_p019_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: VC_Correct Module Type for sll_free in sll_free_goal.v. Although this example can be fully automatically solved by our solver, here we present the Rocq proof for the verification condition discussed in Section 2.2, which is sll_free_entail_wit_2. QCP provides a pre_process command for pre￾processing verification conditions. After preprocessing, the proof becomes [PITH_FULL_IMAGE:figures/full_fig_p019_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: VC_Correctness Module for sll_free in sll_free_proof_check.v. x : Z H : x <> 0 ---------------------------- listrep x ⊢ EX v : Z, EX n : Z, [| x <> 0 |] && &( x # "list" → "next") # Ptr |→ n ** listrep n ** &( x # "list" → "data") # Int |→ v Next, given that x <> 0, which means listrep(x) is non-empty, we can use sep_apply listrep_nonzero to unfold listrep(x) into its non-empty form. The proof then become… view at source ↗
Figure 13
Figure 13. Figure 13: Language Design comparison between RefinedC and QCP. such that any final state after executing mergesortrec(l) satisfies X. In essence, this specification can be interpreted as follows: given a list l stored in a singly linked list at address x, upon termination of the function, we have effectively executed the abstract program mergesortrec(l) and returned l0, which is then stored in the linked list at x.… view at source ↗
Figure 14
Figure 14. Figure 14: Definition of mergesortrec. struct list * merge_sort(struct list * x) /*@ With l X Require safeExec(ATrue, mergesortrec(l), X) && sll(x, l) Ensure exists l0, safeExec(ATrue, return(l0), X) && sll(__return, l0) */; [PITH_FULL_IMAGE:figures/full_fig_p023_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Relational specification of merge sort example [PITH_FULL_IMAGE:figures/full_fig_p023_15.png] view at source ↗
read the original abstract

As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite significant advancements in verification techniques and tools, their practical application to complex, real-world systems is often hindered by critical gaps in both automation and expressiveness. To address these difficulties, this paper presents \textbf{Qualified C Programming Verifier (QCP)}, a novel verification tool that integrates annotation-based automatic verification with interactive proving using Rocq. QCP employs symbolic execution and a separation logic entailment solver to automatically discharge many verification obligations, while deferring more complex obligations to Rocq for manual proof. Furthermore, QCP includes a VS Code extension designed to enhance proof efficiency and support a deeper understanding of both the program behavior and verification outcomes.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents Qualified C Programming Verifier (QCP), a tool integrating annotation-based automatic verification for C programs—via symbolic execution and a separation logic entailment solver—with interactive proving in Rocq, plus a VS Code extension to aid proof efficiency and understanding of program behavior and outcomes. The central goal is addressing gaps in both automation and expressiveness for complex real-world C systems.

Significance. If the automatic component reliably discharges a substantial fraction of verification obligations on realistic code, the hybrid architecture could meaningfully advance practical C verification by combining automation strengths with Rocq's expressiveness for residual cases. The VS Code extension is a concrete usability contribution. However, the manuscript provides neither implementation details nor empirical support, leaving the significance potential rather than established.

major comments (2)
  1. Abstract: the claim that symbolic execution combined with the separation logic entailment solver will 'automatically discharge many verification obligations' is load-bearing for the entire value proposition, yet the manuscript supplies no implementation details, soundness argument for the solver, or quantitative evidence that this occurs on realistic C code rather than toy examples.
  2. No evaluation section: the manuscript reports no metrics on the fraction of VCs discharged automatically, lines of code verified, or case studies involving programs with heavy pointer aliasing, library calls, or size >10kLOC; without such data the practicality claim that only 'manageable' obligations remain for Rocq cannot be assessed.
minor comments (1)
  1. Abstract: the description of the VS Code extension could be expanded with one sentence on its specific features (e.g., how it visualizes obligations or interacts with Rocq) to improve clarity for readers unfamiliar with the workflow.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments and for recognizing the potential of QCP's hybrid architecture. We address the major comments point by point below and will revise the manuscript to strengthen the presentation of implementation details and add supporting evidence where feasible.

read point-by-point responses

  1. Referee: Abstract: the claim that symbolic execution combined with the separation logic entailment solver will 'automatically discharge many verification obligations' is load-bearing for the entire value proposition, yet the manuscript supplies no implementation details, soundness argument for the solver, or quantitative evidence that this occurs on realistic C code rather than toy examples.

    Authors: We agree the claim is central. The full manuscript details the symbolic execution engine and separation logic entailment solver in Sections 3 and 4, including handling of C constructs and integration with Rocq. A soundness sketch appears in Section 5. We acknowledge that a more formal soundness argument and quantitative data would better support the claim. In revision we will expand the soundness discussion and add preliminary results from case studies demonstrating automatic discharge rates on realistic examples. revision: partial

  2. Referee: No evaluation section: the manuscript reports no metrics on the fraction of VCs discharged automatically, lines of code verified, or case studies involving programs with heavy pointer aliasing, library calls, or size >10kLOC; without such data the practicality claim that only 'manageable' obligations remain for Rocq cannot be assessed.

    Authors: We acknowledge the manuscript currently lacks a dedicated evaluation section with quantitative metrics or large-scale case studies. The focus has been on tool design, annotations, and the VS Code extension, illustrated with smaller examples. This is a valid observation. We will add an Evaluation section reporting metrics such as the fraction of VCs discharged automatically, lines of code, and results on programs with pointer aliasing and library calls. For programs exceeding 10kLOC we currently have only smaller-scale experiments, but the hybrid design is intended to leave only complex cases for Rocq. revision: yes

Circularity Check

0 steps flagged

No circularity: tool architecture paper with no derivations or self-referential predictions

full rationale

The manuscript presents QCP as a practical tool combining annotation-based symbolic execution, a separation logic solver, and Rocq for residual obligations. No equations, fitted parameters, or first-principles derivations appear in the provided text. Claims about discharging verification conditions rest on the described architecture and an untested practical assumption rather than any reduction to the paper's own prior outputs or self-citations. The derivation chain is therefore self-contained with no load-bearing steps that collapse by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on standard domain assumptions from separation logic and interactive theorem proving rather than new axioms or fitted parameters introduced in this work.

axioms (2)
  • domain assumption Separation logic provides a sound foundation for reasoning about C program memory and aliasing
    Invoked as the basis for the automatic entailment solver
  • domain assumption Rocq is capable of discharging complex verification obligations that the automatic solver cannot handle
    Assumed from prior successful uses of Rocq in program verification
invented entities (1)
  • QCP tool and its VS Code extension no independent evidence
    purpose: Practical integration of automatic and interactive verification for C
    The tool itself is the primary contribution; no independent evidence outside the paper is supplied

pith-pipeline@v0.9.0 · 5702 in / 1361 out tokens · 57107 ms · 2026-05-22T14:52:42.695350+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages

  1. [1]

    In: Proceedings of the 4th International Confer- ence on Formal Methods for Components and Objects

    Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: Proceedings of the 4th International Confer- ence on Formal Methods for Components and Objects. pp. 115–137. FMCO’05, Springer-Verlag, Berlin, Heidelberg (2005).https://doi.org/10.1007/11804192_ 6

    work page doi:10.1007/11804192_ 2005

  2. [2]

    Beringer, L.: Verified software units. In: Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings. pp. 118–147. Springer-Verlag, Berlin, Heidelberg (2021).https://d...

    work page 2021

  3. [3]

    In: Proceedings of the Third International Conference on NASA Formal Methods

    Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Proceedings of the Third International Conference on NASA Formal Methods. pp. 459–465. NFM’11, Springer-Verlag, Berlin, Heidelberg (2011)

    work page 2011

  4. [4]

    Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: A separa- tionlogictooltoverifycorrectnessofCprograms.JournalofAutomatedReasoning 61(1), 367–422 (Jun 2018).https://doi.org/10.1007/s10817-018-9457-5

    work page doi:10.1007/s10817-018-9457-5 2018

  5. [5]

    In: 10th IEEE High Assurance Systems Engineer- ing Symposium (HASE’07)

    Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Multiple Pre/Post specifications for heap-manipulating methods. In: 10th IEEE High Assurance Systems Engineer- ing Symposium (HASE’07). pp. 357–364 (2007).https://doi.org/10.1109/HASE. 2007.19

    work page doi:10.1109/hase 2007

  6. [6]

    Jour- nal of Combinatorial Theory, Series A14(3), 288–297 (1973).https://doi.org/ https://doi.org/10.1016/0097-3165(73)90004-6

    Dantzig, G.B., Curtis Eaves, B.: Fourier-Motzkin elimination and its dual. Jour- nal of Combinatorial Theory, Series A14(3), 288–297 (1973).https://doi.org/ https://doi.org/10.1016/0097-3165(73)90004-6

    work page doi:10.1016/0097-3165(73)90004-6 1973

  7. [7]

    Facebook: SPARTA: A library of software components designed for building high- performance static analyzers based on the theory of abstract interpretation,https: //github.com/facebook/SPARTA, gitHub repository

    work page

  8. [8]

    Huawei LiteOS: LiteOS kernel.https://github.com/LiteOS/LiteOS

    work page

  9. [9]

    In: Barrett, C., Davies, M., Kahsai, T

    Illous, H., Lemerre, M., Rival, X.: A relational shape abstract domain. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NASA Formal Methods. pp. 212–229. Springer International Publishing, Cham (2017)

    work page 2017

  10. [10]

    In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R

    Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods. pp. 41–55. Springer, Berlin, Heidelberg (2011)

    work page 2011

  11. [11]

    SIG- PLAN Not.51(9), 256–269 (Sep 2016).https://doi.org/10.1145/3022670

    Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. SIG- PLAN Not.51(9), 256–269 (Sep 2016).https://doi.org/10.1145/3022670. 2951943

    work page doi:10.1145/3022670 2016

  12. [12]

    Formal Aspects of Computing27(3), 573–609 (2015)

    Kirchner, F., Cuoq, P., Correnson, L., Prevosto, V., Signoles, J.: Frama-C: A soft- ware analysis perspective. Formal Aspects of Computing27(3), 573–609 (2015). https://doi.org/10.1007/s00165-014-0326-7

    work page doi:10.1007/s00165-014-0326-7 2015

  13. [13]

    Kroening, D., Schrammel, P., Tautschnig, M.: CBMC: The C bounded model checker (2023),https://arxiv.org/abs/2302.02384

    work page arXiv 2023

  14. [14]

    Springer Publishing Company, Incorporated, 1 edn

    Kroening, D., Strichman, O.: Decision procedures: An algorithmic point of view. Springer Publishing Company, Incorporated, 1 edn. (2008)

    work page 2008

  15. [15]

    In: Jobstmann, B., Leino, K.R.M

    Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol. 9583, pp. 41–

    work page

  16. [16]

    Springer-Verlag (2016),https://doi.org/10.1007/978-3-662-49122-5_2 QCP: A C Verification Tool 17

    work page doi:10.1007/978-3-662-49122-5_2 2016

  17. [17]

    In: Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation

    Nguyen, H.H., David, C., Qin, S., Chin, W.N.: Automated verification of shape and size properties via separation logic. In: Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. pp. 251–

    work page

  18. [18]

    VMCAI’07, Springer-Verlag, Berlin, Heidelberg (2007)

    work page 2007

  19. [19]

    Nguyen, Q.L., David, C., Chin, W.N.: Hip/Sleek: Verification system for heap- manipulating programs (Splice example) (2023),https://github.com/hipsleek/ hipsleek/blob/master/benchmark/SV-COMP/list_properties/splice.ss, gitHub repository, benchmark example:splice.ss

    work page 2023

  20. [20]

    In: Proceedings of the 16th International Conference on Term Rewriting and Applications

    Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Proceedings of the 16th International Conference on Term Rewriting and Applications. pp. 453–468. RTA’05, Springer-Verlag, Berlin, Heidelberg (2005).https://doi.org/ 10.1007/978-3-540-32033-3_33

    work page doi:10.1007/978-3-540-32033-3_33 2005

  21. [21]

    Pulte, C., Makwana, D.C., Sewell, T., Memarian, K., Sewell, P., Krishnaswami, N.: CN: Verifying systems C code with separation-logic refinement types. Proc. ACM Program. Lang.7(POPL) (Jan 2023).https://doi.org/10.1145/3571194

    work page doi:10.1145/3571194 2023

  22. [22]

    In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021)

    Sammler, M., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., Garg, D.: Re- finedC: Automating the foundational verification of C code with refined ownership types. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). pp. 158–174. ACM, New York, NY, USA (2021).https://doi.org/1...

    work page doi:10.1145/3453483.3454060 2021

  23. [23]

    Wang, Z., Wu, X., Fang, Y., Li, C., Zhong, H., Xie, L., Cao, Q., Hu, Z.: Stellis: A strategy language for purifying separation logic entailments (2025),https:// arxiv.org/abs/2512.05159

    work page arXiv 2025

  24. [24]

    Wu, S., Wu, X., Cao, Q.: Encode the∀∃relational hoare logic into standard hoare logic. Proc. ACM Program. Lang.9(OOPSLA2) (Oct 2025).https://doi.org/ 10.1145/3763138

    work page doi:10.1145/3763138 2025

  25. [25]

    Zhou, L., Qin, J., Wang, Q., Appel, A.W., Cao, Q.: VST-A: A foundationally sound annotation verifier. Proc. ACM Program. Lang.8(POPL) (Jan 2024).https:// doi.org/10.1145/3632911 A Overview of Stellis Stellis is a domain-specific language (DSL) designed to streamline the automa- tion of separation logic entailment proofs. By enabling users to specify verif...

    work page doi:10.1145/3632911 2024

  26. [26]

    A priorityr, specified using theprioritylabel

    work page

  27. [27]

    A sequence of patternsq

    work page

  28. [28]

    A sequence of checksc, denoted by thechecklabel

    work page

  29. [29]

    existsx, qr

    An actiona, indicated by theactionlabel. The pattern part is used to identify specific formulas on both sides of the entailment. For right patterns, a pattern variablexmay be constrained to bind an existential variable in the entailment via the syntax “existsx, qr”. The pattern formula ˆffollows the same syntactic structure as the formulafin the entailmen...

    work page