Pith. sign in

REVIEW 3 major objections 5 minor 63 references

A partial, caller-sufficient contract is enough for sound regression verification of C patches, and can be inferred automatically from a model checker's own counterexamples.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Caller-sufficient partial contracts, LLM-inferred and verifier-enforced, soundly prove safety-preserving regression equivalence without full behavioral specs.

T0 review reviewed 2026-07-14 challenge →

load-bearing objection Clean one-sided soundness theorem plus a working LLM+BMC pipeline; the termination gap is real but stated, and the empirical claims are careful enough to deserve referee time. the 3 major comments →

arxiv 2607.10291 v1 pith:3MURWQT2 submitted 2026-07-11 cs.SE cs.AI

Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification

Yiannis Charalambous , Rafael Menezes , Youcheng Sun , Lucas C. Cordeiro This is my paper
classification cs.SE cs.AI
keywords regression verificationfunction contractsconditional equivalenceLLM-based specification inferencebounded model checkingassume-guarantee reasoningframe conditionssoftware safety
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The reading

When software is patched, developers need to know whether the change preserves the behavior callers already rely on, without re-checking the whole program or writing full formal specifications by hand. This paper argues that a weak, one-sided function contract is enough: enforce the contract only against the old version so it over-approximates safe behavior, then use it as a modular stand-in while the new version runs concretely, comparing only the outputs a property cares about. That relation, called safety-preserving conditional equivalence, lets intentional bug fixes through while still catching regressions, including new memory and arithmetic safety errors. The contracts themselves are proposed by a language model and certified by the verifier from its own counterexample traces, with no separate specification step. Strengthening those partial contracts further barely increases tightness, so stopping at what the caller needs costs almost nothing, and the underlying check never fabricates an equivalence on a third-party benchmark.

Core claim

A one-sided partial contract that over-approximates only the old function version and is precise on the property-observed outputs is sound for safety-preserving conditional (regression) equivalence: if the contract is enforced against the old function and sufficient for the caller-observed obligation against the new function, then the new version is regression-equivalent to the old on the property's scope. Empirically, such caller-sufficient contracts already capture nearly all attainable tightness under continued strengthening, and the end-to-end pipeline reaches verification rates comparable to prior weakest-precondition contract tools while certifying a stronger property.

What carries the argument

Theorem T1 (soundness of one-sided contract abstraction): enforcement of contract C against the old version plus sufficiency of C for the property-relative obligation against the new version jointly imply property-relative regression equivalence; a depth-bounded call-graph closure lifts the argument modularly without expanding the whole program.

Load-bearing premise

The soundness claim only covers terminating runs, so a change that makes the new version hang where the old one finished is outside the guarantee.

What would settle it

On Frama-C-Problems, keep strengthening past the caller-sufficient seed for many more rounds and show that a large share of orderable targets become strictly tighter under the semantic admit-set comparator; or find a non-equivalent EqBench-C pair that the regression check certifies as equivalent.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Modular regression checks can reuse a single enforced old-version contract at every call site instead of re-analyzing callee bodies.
  • Contract inference can stop at caller-sufficiency without a meaningful loss of tightness relative to further strengthening within the same clause shape.
  • A passing result certifies enforcement plus caller-sufficiency with runtime-error freedom included, not merely a syntactic annotation count.
  • Counterexample traces from a bounded model checker alone can drive frame and postcondition inference competitively with weaker-precondition feedback loops.
  • The same soundness oracle can surface mislabeled equivalent pairs in public equivalence benchmarks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the depth-bounded closure works on larger call graphs, teams could re-verify only the changed stratum of a long-lived C codebase after each patch rather than the whole tree.
  • The same one-sided partial-contract idea is a natural candidate for languages with richer signatures once alignment across parameter reorderings and splits is solved.
  • A production workflow could run the cheap contract-free check first and escalate only timeouts to LLM-inferred contracts, treating remaining false alarms as triage rather than blockers.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper presents the first contract-based regression-verification pipeline for C. It proves (Theorem T1) that a one-sided partial contract enforced only against the old version and sufficient for a property-relative obligation against the new version yields safety-preserving conditional (regression) equivalence, with a depth-bounded lift (Lemma L1). Contracts are inferred by an LLM propose-and-certify loop (SCRIBE) driven by ESBMC counterexamples, then used modularly by REGVER; JUDGE decides admit-set inclusion between contracts. Empirically, on Frama-C-Problems and six ANSSI X509 functions the inference rate is comparable to AutoSpec/Preguss while certifying a stronger property; strengthening past caller-sufficiency barely tightens contracts (RQ2); on EqBench-C the checker reports zero fabricated equivalences on decided pairs and surfaces nine mislabeled Eq pairs.

Significance. If the result holds, the paper gives a clean modular foundation for regression verification that does not require full behavioral specs or whole-program re-analysis, and shows that LLM-inferred partial contracts can be made trustworthy by verifier enforcement. Strengths that should be credited: a short, standard assume-guarantee proof of T1 with an explicit depth-N closure; a reusable semantic tightness comparator (JUDGE/T2) rather than syntactic annotation counts; automatic CE-driven inference with no hand-written specs; and a careful soundness check on third-party EqBench-C that never fabricates an equivalence and finds more mislabels than concurrent work. The partial-spec stopping point is both theoretically motivated and empirically supported on the orderable subset.

major comments (3)
  1. [§IV-A (A1), Definitions 5–6, Abstract] §IV-A, standing assumption (A1) and Definitions 5–6: the relational semantics only populate terminating runs, so a change that makes f2 diverge where f1 terminated and satisfied ϕ is outside the guarantee. The paper states this and defers termination regressions to future work, but the marketed property name “safety-preserving conditional equivalence” (abstract, §I, §VI) can be read as covering a broader class of regressions than the theorem delivers. Either restrict the claim language to partial-correctness / RTE-preserving conditional equivalence throughout, or add a prominent limitations paragraph that states which realistic regression modes (non-termination, livelock) are not covered and why EqBench-C cannot stress them.
  2. [§V-E2, Table III, Figure 3, RQ2 Answer] §V-E2 / Table III / Figure 3 (RQ2): about 40% of round-level comparisons are held out because JUDGE cannot order quantified or pointer-dereferencing postconditions, and the saturation curves fix the denominator to the always-orderable subset (16/18/19 targets). The headline claim that “partial-spec contracts capture nearly all the attainable tightness” and “stopping at caller-sufficiency costs almost nothing” is therefore established only on that subset. Please report the fraction of all successfully inferred contracts that are orderable, give a sensitivity analysis or qualitative discussion of the unorderable cases, and qualify the abstract/RQ2 answer so it does not over-generalize from the orderable majority.
  3. [§V-E3, Table IV] §V-E3 / Table IV: the contract arm recovers 7–11 additional correct decisions on the undecided EqBench-C tail but roughly triples false positives (14 → ~38–40). Soundness (no fabricated equivalences) is preserved, yet the practical claim that contracts “earn their keep” needs a clearer cost–benefit discussion: how a developer should triage the FP-heavy tail, whether a precision/recall trade-off or confidence signal is available, and whether the portfolio is recommended as a default workflow or only as a soundness oracle. Without that, the reach numbers can be misread as a net win.
minor comments (5)
  1. [Figure 2] Figure 2 caption says “RQ3 convergence histogram” while the section is RQ1; renumber consistently.
  2. [Table I] Table I: make the dual reporting (decided vs. conservative) explicit in the column header or a footnote so readers do not confuse 85.7% with the full-denominator rate.
  3. [§III-A] §III: a short explicit contrast with impact-summary regression verification [26] on reusability vs. path-condition exactness would help readers place the one-sided contract contribution.
  4. [§IV-D] JUDGE’s frame containment is “syntactic in v1” (§IV-D, §V-G); state this limitation once near Theorem T2 so the refinement claim is not over-read for frames.
  5. [Definition 3, §V] Minor typos: “oagrees” spacing in Definition 3; “HARDSCRIBE” appears without prior expansion in §V-D/E.

Circularity Check

0 steps flagged

No significant circularity: Theorem T1 is a self-contained mathematical derivation from explicit definitions and standing assumptions; empirical claims rest on third-party suites and an independent verifier.

full rationale

The load-bearing derivation is Theorem T1 (soundness of one-sided contract abstraction) together with Definitions 5–6 and the short direct proof in §IV-A: enforcement places the real old-version output inside the contract’s admit set, so the sufficiency quantifier specializes to it. The proof uses only the relational semantics of Definition 1, the admit-set semantics of Definition 3, and the three standing assumptions (A1–A3); none of those definitions or assumptions is defined in terms of the conclusion, fitted to the target data, or imported via a uniqueness claim from the authors’ prior work. Depth-bounded closure (Lemma L1) is likewise an ordinary inductive argument on the call graph. Contract inference is propose-and-certify: the LLM is never trusted, only ESBMC-enforced contracts are used, and success is measured against external oracles (Frama-C-Problems, ANSSI X509, EqBench-C). JUDGE is a relative admit-set inclusion test paired with separate enforcement, not a self-justifying metric. Minor citations to overlapping-author tooling appear in related work and the system description but are not premises of T1 or of the soundness claim on EqBench-C. Consequently the central result does not reduce by construction to its inputs, and the paper scores 0 on circularity.

Axiom & Free-Parameter Ledger

4 free parameters · 5 axioms · 3 invented entities

The central claim rests on standard Hoare/frame reasoning plus three standing assumptions (termination, frame soundness under aliasing, verifier soundness), the ESBMC safety encoding as the property ϕ, and engineering knobs (depth N, iteration/timeout budgets, temperature 0). No new physical entities are postulated; the invented pieces are methodological (tools, the named equivalence notion, JUDGE).

free parameters (4)
  • contract-closure depth N
    Configurable bound on how deep partial contracts are inferred; trades precision for scalability (Lemma L1). Chosen by the user/system, not derived.
  • max refinement iterations (5)
    Hard cap on SCRIBE’s propose-and-enforce loop; affects whether a contract is found within budget.
  • per-query ESBMC and LLM timeouts (300s)
    Fixed experimental budgets that determine the undecided EqBench-C tail and non-result rates.
  • LLM temperature (0) and model choice
    Single deterministic trajectory per model; different seeds/models can shift individual inference cases though telemetry is reported as near-identical across three models.
axioms (5)
  • domain assumption Partial correctness: only terminating runs populate [f]; termination regressions are out of scope (A1).
    Stated in §IV-A; required for Theorem T1’s relational model.
  • domain assumption Frame rule is sound even under aliasing: enforcement implies no writes outside Assigns (A2).
    Standing assumption for contract enforcement/replacement; honest unknown if violated.
  • domain assumption The underlying verifier (ESBMC enforce/replace) is sound for the relational contract model (A3).
    Theorem T1 is verifier-independent but the implementation inherits ESBMC’s soundness.
  • standard math External nondeterminism is folded into the shared input pre-state so both versions see the same responses.
    Definition 1; standard for relational/equivalence reasoning.
  • domain assumption ϕ is instantiated as ESBMC’s safety property set (memory safety, div-by-zero, overflow, leaks, UB shifts).
    Implementation choice that defines the scope Sc of safety-preserving conditional equivalence.
invented entities (3)
  • safety-preserving conditional equivalence independent evidence
    purpose: Name the target relation: enforcement plus caller-sufficiency with runtime-error freedom via the safety encoding.
    A named specialization of conditional/regression equivalence; definitional rather than a physical postulate, but central to claim strength.
  • JUDGE semantic contract-tightness comparator independent evidence
    purpose: Decide admit-set inclusion between contracts and report equivalent/tighter/incomparable with witnesses.
    New methodological artifact (C3); independent of any single LLM run once contracts are fixed.
  • SCRIBE / CONTRACTOR / REGVER pipeline no independent evidence
    purpose: End-to-end inference and regression checking with one-sided contracts.
    System contribution (C2); evaluated on public benchmarks but not independently reimplemented in the paper.

reviewed 2026-07-14 · how reviews work

0 comments
Cite this review

Pith. "Pith review of Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification." pith.science (2026). https://pith.science/paper/3MURWQT2

@misc{pith2026260710291,
  author       = {Pith},
  title        = {Pith review of: Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3MURWQT2}},
  note         = {Machine review of arXiv:2607.10291}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Software evolves continuously, yet ensuring that a patch preserves intended behavior without re-verifying an entire codebase remains difficult. Regression verification addresses this problem, but existing techniques require expensive whole-program reasoning or rely on manually written specifications that are rarely available in practice. We present the first contract-based regression verification tool. Contract soundness is ensured by proving all function versions match the behavior. The contract then verifies program flow via assume-guarantee. We ask whether a partial, caller-sufficient contract, rather than a full behavioral specification, is enough. On Frama-C-Problems we strengthen each inferred contract past what the caller needs and measure how much tighter it becomes. It barely moves: for most targets in every model the caller-sufficient contract is already the tightest the loop reaches, and our tightness comparator rates the partial and strengthened contracts equivalent for the large majority of targets it can compare. Partial-spec contracts thus capture nearly all the attainable tightness, so stopping at caller-sufficiency costs almost nothing. The regression check underneath is sound: on the third-party EqBench-C suite it never fabricates an equivalence, returning zero false proofs and reporting an unprovable difference instead. It also surfaced nine pairs that EqBench mislabels as equivalent, more than a concurrent tool reports. The contracts themselves are inferred automatically from the checker's own counterexamples, with no separate specification step; on Frama-C-Problems and the ANSSI X509 parser this reaches a verification rate comparable to tools AutoSpec and Preguss, while a passing result certifies at least as strong a property, which we call \emph{safety-preserving conditional equivalence}: enforcement plus caller-sufficiency.

Figures

Figures reproduced from arXiv: 2607.10291 by Lucas C. Cordeiro, Rafael Menezes, Yiannis Charalambous, Youcheng Sun.

Figure 1
Figure 1. Figure 1: A property-relative regression check. The fix corrects [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: RQ1 convergence histogram per model on Frama-C-Problems: the [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: RQ2 tightness saturation on Frama-C-Problems. Per model, the share [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Contract-free baseline regression-verification outcomes on EqBench-C. [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗

discussion (0)

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

Reference graph

Works this paper leans on

63 extracted references · 7 canonical work pages

  1. [1]

    How do fixes become bugs?

    Z. Yin, D. Yuan, Y . Zhou, S. Pasupathy, and L. Bairavasundaram, “How do fixes become bugs?” inProceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, ser. ESEC/FSE ’11. New York, NY , USA: Association for Computing Machinery, 2011, p. 26–36. [Online]. Available: https://doi.org/10.1145/202511...

    doi:10.1145/2025113.2025121 2011

  2. [2]

    Classes of recursively enumerable sets and their decision problems,

    H. G. Rice, “Classes of recursively enumerable sets and their decision problems,”Transactions of the American Mathematical Society, vol. 74, no. 2, pp. 358–366, 1953. [Online]. Available: http://www.jstor.org/stable/1990888

    arXiv 1953

  3. [3]

    Regression verification: proving the equivalence of similar programs,

    B. Godlin and O. Strichman, “Regression verification: proving the equivalence of similar programs,”Software Testing, Verification and Reliability, vol. 23, no. 3, pp. 241–258, 2013. [Online]. Available: https://onlinelibrary.wiley.com/doi/abs/10.1002/stvr.1472

    work page doi:10.1002/stvr.1472 2013

  4. [4]

    Enchanting program specification synthesis by large language models using static analysis and program verification,

    C. Wen, J. Cao, J. Su, Z. Xu, S. Qin, M. He, H. Li, S.-C. Cheung, and C. Tian, “Enchanting program specification synthesis by large language models using static analysis and program verification,” inComputer Aided Verification, A. Gurfinkel and V . Ganesh, Eds. Cham: Springer Nature Switzerland, 2024, pp. 302–328

    2024

  5. [5]

    Specify what? enhancing neural specification synthesis by symbolic methods,

    G. Granberry, W. Ahrendt, and M. Johansson, “Specify what? enhancing neural specification synthesis by symbolic methods,” inIntegrated Formal Methods, N. Kosmatov and L. Kov ´acs, Eds. Cham: Springer Nature Switzerland, 2025, pp. 307–325

    2025

  6. [6]

    A tale of 1001 loc: Potential runtime error-guided specification synthesis for verifying large-scale programs,

    Z. Wang, T. Lin, M. Chen, H. Li, M. Yang, X. Yi, S. Qin, Y . Luo, X. Li, B. Gu, L. Lu, and J. Yin, “A tale of 1001 loc: Potential runtime error-guided specification synthesis for verifying large-scale programs,”Proc. ACM Program. Lang., vol. 10, no. OOPSLA1, Apr

  7. [7]

    Available: https://doi.org/10.1145/3798268

    [Online]. Available: https://doi.org/10.1145/3798268

    work page doi:10.1145/3798268

  8. [8]

    Regression verification,

    B. Godlin and O. Strichman, “Regression verification,” inProceedings of the 46th Annual Design Automation Conference, ser. DAC ’09. New York, NY , USA: Association for Computing Machinery, 2009, p. 466–471. [Online]. Available: https://doi.org/10.1145/1629911.1630034

    doi:10.1145/1629911.1630034 2009

  9. [9]

    An axiomatic basis for computer programming,

    C. A. R. Hoare, “An axiomatic basis for computer programming,” Commun. ACM, vol. 12, no. 10, p. 576–580, Oct. 1969. [Online]. Available: https://doi.org/10.1145/363235.363259

    doi:10.1145/363235.363259 1969

  10. [10]

    Applying ’design by contract’,

    B. Meyer, “Applying ’design by contract’,”Computer, vol. 25, no. 10, pp. 40–51, 1992

    1992

  11. [11]

    Automating regression verification,

    D. Felsing, S. Grebing, V . Klebanov, P. R ¨u mmer, and M. Ulbrich, “Automating regression verification,” inProceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ser. ASE ’14. New York, NY , USA: Association for Computing Machinery, 2014, p. 349–360. [Online]. Available: https://doi.org/10.1145/2642937.2642987

    doi:10.1145/2642937.2642987 2014

  12. [12]

    Automating regression veri- fication of pointer programs by predicate abstraction,

    V . Klebanov, P. R¨ummer, and M. Ulbrich, “Automating regression veri- fication of pointer programs by predicate abstraction,”Formal Methods in System Design, vol. 52, no. 3, pp. 229–259, 2018

    2018

  13. [13]

    Symdiff: A language-agnostic semantic diff tool for imperative programs,

    S. K. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Reb ˆelo, “Symdiff: A language-agnostic semantic diff tool for imperative programs,” in Computer Aided Verification, P. Madhusudan and S. A. Seshia, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 712–717

    2012

  14. [14]

    Differential assertion checking,

    S. K. Lahiri, K. L. McMillan, R. Sharma, and C. Hawblitzel, “Differential assertion checking,” inProceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ser. ESEC/FSE 2013. New York, NY , USA: Association for Computing Machinery, 2013, p. 345–355. [Online]. Available: https://doi.org/10.1145/2491411.2491452

    work page doi:10.1145/2491411.2491452 2013

  15. [15]

    Towards modularly comparing programs using automated theorem provers,

    C. Hawblitzel, M. Kawaguchi, S. K. Lahiri, and H. Reb ˆelo, “Towards modularly comparing programs using automated theorem provers,” in Automated Deduction – CADE-24, M. P. Bonacina, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 282–299

    2013

  16. [16]

    Ardiff: scaling program equivalence checking via iterative abstraction and refinement of common code,

    S. Badihi, F. Akinotcho, Y . Li, and J. Rubin, “Ardiff: scaling program equivalence checking via iterative abstraction and refinement of common code,” inProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ser. ESEC/FSE 2020. New York, NY , USA: Association for Comp...

    doi:10.1145/3368089.3409757 2020

  17. [17]

    Peqcheck: Localized and context-aware checking of functional equivalence,

    M.-C. Jakobs, “Peqcheck: Localized and context-aware checking of functional equivalence,” in2021 IEEE/ACM 9th International Confer- ence on Formal Methods in Software Engineering (FormaliSE), 2021, pp. 130–140

    2021

  18. [18]

    Peqtest: Testing functional equivalence,

    M.-C. Jakobs and M. Wiesner, “Peqtest: Testing functional equivalence,” inFundamental Approaches to Software Engineering, E. B. Johnsen and M. Wimmer, Eds. Cham: Springer International Publishing, 2022, pp. 184–204

    2022

  19. [19]

    Pasda: A partition-based semantic differencing approach with best effort classification of undecided cases,

    J. Glock, J. Pichler, and M. Pinzger, “Pasda: A partition-based semantic differencing approach with best effort classification of undecided cases,”Journal of Systems and Software, vol. 213, p. 112037, 2024. [Online]. Available: https://www.sciencedirect.com/science/article/pii/ S0164121224000803

    2024

  20. [20]

    Differential symbolic execution,

    S. Person, M. B. Dwyer, S. Elbaum, and C. S. Pundefinedsundefinedreanu, “Differential symbolic execution,” in Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ser. SIGSOFT ’08/FSE-16. New York, NY , USA: Association for Computing Machinery, 2008, p. 226–237. [Online]. Available: https://doi.org/10.1145/14...

    doi:10.1145/1453101.1453131 2008

  21. [21]

    Shadow of a doubt: testing for divergences between software versions,

    H. Palikareva, T. Kuchta, and C. Cadar, “Shadow of a doubt: testing for divergences between software versions,” inProceedings of the 38th International Conference on Software Engineering, ser. ICSE ’16. New York, NY , USA: Association for Computing Machinery, 2016, p. 1181–1192. [Online]. Available: https://doi.org/10.1145/2884781. 2884845

    doi:10.1145/2884781 2016

  22. [22]

    Strengthening supply chain security with fine-grained safe patch identification,

    C. Luo, W. Meng, and S. Wang, “Strengthening supply chain security with fine-grained safe patch identification,” inProceedings of the IEEE/ACM 46th International Conference on Software Engineering, ser. ICSE ’24. New York, NY , USA: Association for Computing Machinery,

  23. [23]

    Available: https://doi.org/10.1145/3597503.3639104

    [Online]. Available: https://doi.org/10.1145/3597503.3639104

    doi:10.1145/3597503.3639104

  24. [24]

    cozy: Comparative symbolic execution for binary programs,

    C. Helbling, G. Leach-Krouse, S. Lasser, and G. Sullivan, “cozy: Comparative symbolic execution for binary programs,” inProceedings 2025 Workshop on Binary Analysis Research, ser. BAR 2025. Internet Society, 2025. [Online]. Available: http://dx.doi.org/10.14722/bar.2025. 23004

    work page doi:10.14722/bar.2025 2025

  25. [25]

    Mokav: Execution-driven differential testing with llms,

    K. Etemadi, B. Mohammadi, Z. Su, and M. Monperrus, “Mokav: Execution-driven differential testing with llms,” p. 112571, 2025. [Online]. Available: https://www.sciencedirect.com/science/article/pii/ S0164121225002407

    2025

  26. [26]

    Unittenx: Generating tests for legacy packages with ai agents powered by formal verification,

    Y . Charalambous, C. N. C. Jr, L. Lamb, and L. C. Cordeiro, “Unittenx: Generating tests for legacy packages with ai agents powered by formal verification,” 2025. [Online]. Available: https://arxiv.org/abs/2510.05441

    arXiv 2025

  27. [27]

    Quantitative symbolic patch impact analysis,

    L. Sarker, A. Satter, and T. Bultan, “Quantitative symbolic patch impact analysis,” Cham, pp. 367–390, 2026

    2026

  28. [28]

    Regression verifica- tion using impact summaries,

    J. Backes, S. Person, N. Rungta, and O. Tkachuk, “Regression verifica- tion using impact summaries,” inModel Checking Software, E. Bartocci and C. R. Ramakrishnan, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 99–116

    2013

  29. [29]

    A new era in software security: Towards self-healing software via large language models and formal verification,

    N. Tihanyi, Y . Charalambous, R. Jain, M. A. Ferrag, and L. C. Cordeiro, “A new era in software security: Towards self-healing software via large language models and formal verification,” pp. 136–147, 2025

    2025

  30. [30]

    Beyond postconditions: Can large language models infer formal contracts for automatic software verification?

    C. Richter and H. Wehrheim, “Beyond postconditions: Can large language models infer formal contracts for automatic software verification?” 2025. [Online]. Available: https://arxiv.org/abs/2510. 12702

    2025

  31. [31]

    Conver: Using contracts and loop invariant synthesis for scalable formal software verification,

    M. A. A. Pirzada, W. Wang, Y . Charalambous, K. Korovin, and L. C. Cordeiro, “Conver: Using contracts and loop invariant synthesis for scalable formal software verification,” 2026. [Online]. Available: https://arxiv.org/abs/2605.27051

    Pith/arXiv arXiv 2026

  32. [32]

    Autodeduct: A tool for automated deductive verification of c code,

    J. Amilon, D. Gurov, C. Lidstr ¨om, M. Nyberg, G. Ung, and O. Wingbrant, “Autodeduct: A tool for automated deductive verification of c code,” 2025. [Online]. Available: https://arxiv.org/abs/2501.10889

    Pith/arXiv arXiv 2025

  33. [33]

    Amilon, Z

    J. Amilon, Z. Esen, D. Gurov, C. Lidstr ¨om, and P. R ¨ummer,An Exercise in Mind Reading: Automatic Contract Inference for Frama-C. Cham: Springer International Publishing, 2024, pp. 553–582. [Online]. Available: https://doi.org/10.1007/978-3-031-55608-1 13

    doi:10.1007/978-3-031-55608-1 2024

  34. [34]

    Automatic inference of frame axioms using static analysis,

    Z. Rakamaric and A. J. Hu, “Automatic inference of frame axioms using static analysis,” in2008 23rd IEEE/ACM International Conference on Automated Software Engineering, 2008, pp. 89–98

    2008

  35. [35]

    Compositional shape analysis by means of bi-abduction,

    C. Calcagno, D. Distefano, P. O’Hearn, and H. Yang, “Compositional shape analysis by means of bi-abduction,” inProceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’09. New York, NY , USA: Association for Computing Machinery, 2009, p. 289–300. [Online]. Available: https://doi.org/10.1145/1480881.1480917

    doi:10.1145/1480881.1480917 2009

  36. [36]

    Quiver: Guided abductive inference of separation logic specifications in coq,

    S. Spies, L. G ¨aher, M. Sammler, and D. Dreyer, “Quiver: Guided abductive inference of separation logic specifications in coq,”Proc. ACM Program. Lang., vol. 8, no. PLDI, Jun. 2024. [Online]. Available: https://doi.org/10.1145/3656413

    work page doi:10.1145/3656413 2024

  37. [37]

    Evaluating llm-generated acsl annotations for formal verification,

    A. Beg, D. O’Donoghue, and R. Monahan, “Evaluating llm-generated acsl annotations for formal verification,” 2026. [Online]. Available: https://arxiv.org/abs/2602.13851

    Pith/arXiv arXiv 2026

  38. [38]

    Llm meets bounded model checking: Neuro-symbolic loop invariant inference,

    G. Wu, W. Cao, Y . Yao, H. Wei, T. Chen, and X. Ma, “Llm meets bounded model checking: Neuro-symbolic loop invariant inference,” inProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’24. New York, NY , USA: Association for Computing Machinery, 2024, p. 406–417. [Online]. Available: https://doi.org/10.1145...

    doi:10.1145/3691620.3695014 2024

  39. [39]

    Clause2inv: A generate-combine-check framework for loop invariant inference,

    W. Cao, G. Wu, T. Xu, Y . Yao, H. Wei, T. Chen, and X. Ma, “Clause2inv: A generate-combine-check framework for loop invariant inference,”Proc. ACM Softw. Eng., vol. 2, no. ISSTA, Jun. 2025. [Online]. Available: https://doi.org/10.1145/3728920

    doi:10.1145/3728920 2025

  40. [40]

    Bali: Branch-aware loop invariant inference with large language models,

    M. Wang, J. Wang, and X. Cheng, “Bali: Branch-aware loop invariant inference with large language models,” 2025. [Online]. Available: https://arxiv.org/abs/2601.00882

    arXiv 2025

  41. [41]

    Cill: Cti-guided invariant generation via llms for model checking,

    Y . Su, T. Bu, Q. Yang, Y . Ci, and E. Tian, “Cill: Cti-guided invariant generation via llms for model checking,” 2026. [Online]. Available: https://arxiv.org/abs/2602.23389

    arXiv 2026

  42. [42]

    Dafnypro: Llm-assisted automated verification for dafny programs,

    D. Banerjee, O. Bouissou, and S. Zetzsche, “Dafnypro: Llm-assisted automated verification for dafny programs,” 2026. [Online]. Available: https://arxiv.org/abs/2601.05385

    arXiv 2026

  43. [43]

    dafny-annotator: Ai- assisted verification of dafny programs,

    G. Poesia, C. Loughridge, and N. Amin, “dafny-annotator: Ai- assisted verification of dafny programs,” 2024. [Online]. Available: https://arxiv.org/abs/2411.15143

    Pith/arXiv arXiv 2024

  44. [44]

    Inferring multiple helper dafny assertions with llms,

    ´Alvaro Silva, A. Mendes, and R. Martins, “Inferring multiple helper dafny assertions with llms,” 2025. [Online]. Available: https://arxiv.org/abs/2511.00125

    arXiv 2025

  45. [45]

    Quokka: Accelerating program verification with LLMs via invariant synthesis,

    A. Wei, T. Sun, T. Suresh, H. Wu, K. Wang, and A. Aiken, “Quokka: Accelerating program verification with LLMs via invariant synthesis,” 2026. [Online]. Available: https://openreview.net/forum?id= R57hlMlpkm

    2026

  46. [46]

    Program synthesis by sketching,

    A. Solar-Lezama, “Program synthesis by sketching,” Ph.D. dissertation, University of California, Berkeley, 2008

    2008

  47. [47]

    Learning invariants using decision trees and implication counterexamples,

    P. Garg, D. Neider, P. Madhusudan, and D. Roth, “Learning invariants using decision trees and implication counterexamples,” inProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’16. New York, NY , USA: Association for Computing Machinery, 2016, p. 499–512. [Online]. Available: https://doi.org/10.1...

    doi:10.1145/2837614.2837664 2016

  48. [48]

    Data-driven precondition inference with learned features,

    S. Padhi, R. Sharma, and T. Millstein, “Data-driven precondition inference with learned features,” inProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’16. New York, NY , USA: Association for Computing Machinery, 2016, p. 42–56. [Online]. Available: https://doi.org/10.1145/2908080.2908099

    doi:10.1145/2908080.2908099 2016

  49. [49]

    Learning loop invariants for program verification,

    X. Si, H. Dai, M. Raghothaman, M. Naik, and L. Song, “Learning loop invariants for program verification,” inAdvances in Neural Information Processing Systems, S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, Eds., vol. 31. Curran Associates, Inc., 2018. [Online]. Available: https://proceedings.neurips.cc/paper files/paper...

    2018

  50. [50]

    Efficient detection of vacuity in actl formulas,

    I. Beer, S. Ben-David, C. Eisner, and Y . Rodeh, “Efficient detection of vacuity in actl formulas,” inComputer Aided Verification, O. Grumberg, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 1997, pp. 279–290

    1997

  51. [51]

    A behavioral notion of subtyping,

    B. H. Liskov and J. M. Wing, “A behavioral notion of subtyping,” ACM Trans. Program. Lang. Syst., vol. 16, no. 6, p. 1811–1841, Nov

  52. [52]

    Available: https://doi.org/10.1145/197320.197383

    [Online]. Available: https://doi.org/10.1145/197320.197383

    doi:10.1145/197320.197383

  53. [53]

    Back and J

    R. Back and J. von Wright,Refinement Calculus - A Systematic Introduction, ser. Graduate Texts in Computer Science. Springer,

  54. [54]

    Available: https://doi.org/10.1007/978-1-4612-1674-2

    [Online]. Available: https://doi.org/10.1007/978-1-4612-1674-2

    work page doi:10.1007/978-1-4612-1674-2

  55. [55]

    Eqbench: A dataset of equivalent and non-equivalent program pairs,

    S. Badihi, Y . Li, and J. Rubin, “Eqbench: A dataset of equivalent and non-equivalent program pairs,” in2021 IEEE/ACM 18th International Conference on Mining Software Repositories (MSR), 2021, pp. 610–614

    2021

  56. [56]

    EquiBench: Benchmarking large language models’ reasoning about program semantics via equivalence checking,

    A. Wei, J. Cao, R. Li, H. Chen, Y . Zhang, Z. Wang, Y . Liu, T. S. F. X. Teixeira, D. Yang, K. Wang, and A. Aiken, “EquiBench: Benchmarking large language models’ reasoning about program semantics via equivalence checking,” Suzhou, China, pp. 33 868–33 881, Nov. 2025. [Online]. Available: https://aclanthology.org/2025.emnlp-main.1718/

    2025

  57. [57]

    A repository dedicated for problems related to verification of programs using the tool Frama-C,

    M. Patnaik, “A repository dedicated for problems related to verification of programs using the tool Frama-C,” https://github.com/manavpatnaik/ frama-c-problems, 2020, accessed: 2026-06

    2020

  58. [58]

    (2026, 5) Introducing claude opus 4.8

    Anthropic. (2026, 5) Introducing claude opus 4.8. [Online]. Available: https://www.anthropic.com/news/claude-opus-4-8

    2026

  59. [59]

    (2026) moonshotai/kimi-k2.6

    Moonshot AI. (2026) moonshotai/kimi-k2.6. [Online]. Available: https://huggingface.co/moonshotai/Kimi-K2.6

    2026

  60. [60]

    Qwen3.6-27B: Flagship-level coding in a 27B dense model,

    Qwen Team, “Qwen3.6-27B: Flagship-level coding in a 27B dense model,” April 2026. [Online]. Available: https://qwen.ai/blog?id=qwen3. 6-27b

    2026

  61. [61]

    Mislabeled equivalent pairs in EqBench-C,

    Y . Charalambous, “Mislabeled equivalent pairs in EqBench-C,” Issue #15,shrBadihi/EqBenchGitHub repository, 2026, https://github. com/shrBadihi/EqBench/issues/15

    2026

  62. [62]

    Svf: interprocedural static value-flow analysis in llvm,

    Y . Sui and J. Xue, “Svf: interprocedural static value-flow analysis in llvm,” inProceedings of the 25th International Conference on Compiler Construction, ser. CC ’16. New York, NY , USA: Association for Computing Machinery, 2016, p. 265–266. [Online]. Available: https://doi.org/10.1145/2892208.2892235

    doi:10.1145/2892208.2892235 2016

  63. [63]

    Documenting and automating collateral evolutions in linux device drivers,

    Y . Padioleau, J. Lawall, R. R. Hansen, and G. Muller, “Documenting and automating collateral evolutions in linux device drivers,” in Proceedings of the 3rd ACM SIGOPS/EuroSys European Conference on Computer Systems 2008, ser. Eurosys ’08. New York, NY , USA: Association for Computing Machinery, 2008, p. 247–260. [Online]. Available: https://doi.org/10.11...

    work page doi:10.1145/1352592.1352618 2008

This paper was first reviewed by grok-4.5 on July 14, 2026.