Pith. sign in

REVIEW 3 major objections 6 minor 52 references

InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs

T0 review · 3 major / 6 minor · reviewed 2026-07-11 · grok-4.5

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

Pith's one-line read InvWeaver synthesizes loop invariants for multi-loop programs by exposing inter-loop dependencies and propagating weakest-precondition proof obligations.

desk verdict Solid multi-loop engineering with a real failure mode and strong tables; the 32-problem margin is not yet independently checkable because CLRS-Alg and the baseline extensions are author-side. read the letter →

arxiv 2607.05478 v1 pith:IYRREW2V submitted 2026-07-06 cs.LG cs.PL

Guangyuan Wu , Weining Cao , Zehui Tan , Yuan Yao , Hengfeng Wei , Taolue Chen , Xiaoxing Ma This is my paper
classification cs.LGcs.PL
keywords loopinvariantsprogramverificationmulti-loopprogramslargelanguagemodelsweakestpreconditionneuro-symbolicmethodsACSLCLRSalgorithms
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Programs with nested or sequential loops often break automatic verification because each loop is under-specified in isolation: local invariants can look correct yet fail to support the global proof. InvWeaver is a neuro-symbolic method that first builds a loop-level call graph capturing state transitions and verification dependencies among loops, then asks a large language model for candidate ACSL invariants under those local proof contexts, and finally uses weakest-precondition calculus to turn failed obligations into explicit repair targets that are propagated across dependent loops. On a suite that includes a new CLRS-derived algorithmic benchmark, the system solves 72 of 82 multi-loop problems—far more than prior tools—while remaining competitive on single-loop tasks. A sympathetic reader cares because classic algorithms and real software are full of interacting loops, and a method that can weave their invariants into a coherent inductive chain would make formal verification practical for far more everyday code.

What carries the argument

The loop-level call graph (LCG) together with WP-guided dependency-propagating refinement: the LCG supplies the structured verification context for each loop, while weakest-precondition calculus converts each failed establishment, preservation or provability obligation into a concrete logical target that is used both to diagnose the responsible loop and to drive joint repair of dependent invariants.

What would settle it

Run the full InvWeaver pipeline on the 82 multi-loop benchmarks (especially the 58 CLRS-Alg instances) with the same LLMs and solvers; if it fails to solve substantially more problems than AutoSpec and the other listed baselines, or if the ablations that remove obligation-guided inference or WP refinement close most of the gap, the central performance claim is false.

Watch

Extended reading notes

Core claim

The central claim is that local under-specification is the main obstacle for LLM-based invariant inference on multi-loop programs, and that it can be overcome by (1) abstracting the program into a loop-level call graph that records both control-flow state transfers and proof-obligation dependencies, (2) scheduling obligation-guided, top-down or boundary-inward inference so each loop receives the right local pre- and post-conditions, and (3) diagnosing failures with weakest-precondition targets and propagating refinements along the dependency edges until the whole proof chain closes.

Load-bearing premise

Once the language model produces the right ACSL invariants, Frama-C’s weakest-precondition plugin and ordinary SMT solvers can discharge the three Hoare obligations, even though the toolchain does not support dynamic allocation or separation logic.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 6 minor

Summary. The paper presents InvWeaver, a neuro-symbolic framework for synthesizing loop invariants in programs with nested or sequential interacting loops. It builds a loop-level call graph (LCG) that records state-transition and verification-dependency edges, schedules obligation-guided LLM inference top-down / boundary-inward with local pre/post contexts, and uses weakest-precondition (WP) calculus plus LLM diagnosis to propagate and repair failed establishment/preservation/provability obligations across dependent loops, with delayed filtering of irrecoverable candidates. Evaluation on multi-loop and single-loop suites (OOPSLA-13, SV-COMP, and a new CLRS-Alg suite of classic algorithms) reports 72/82 multi-loop solves (at least 32 more than AutoSpec) and 68/70 single-loop solves, with ablations over three LLM backends supporting the roles of obligation-guided inference and WP-guided refinement.

Significance. Loop invariant inference for multi-loop programs is a genuine and under-served bottleneck for LLM-aided verification; the bubble-sort motivation and the LCG + WP-propagation design are a clear conceptual advance over local guess-and-check. If the headline multi-loop margin holds under independent re-evaluation, the work would be a substantial empirical and methodological contribution, especially via the CLRS-Alg suite that targets quantified algorithmic properties rather than purely numerical invariants. Strengths include a principled use of WP as constructive (not merely rejective) feedback, multi-backend ablations (Table III), and explicit discussion of Frama-C/WP limits (§VI). The contribution is therefore significant conditional on reproducible benchmarks and fair multi-loop baseline protocols.

major comments (3)
  1. Table I and §V.A.1–V.A.2: the central claim (72/82 multi-loop solves, ≥32 over AutoSpec, 48 of them on CLRS-Alg) is not independently checkable. CLRS-Alg (58 multi-loop instances) is newly curated with author-written ACSL contracts and ground-truth invariants that are not released; without the suite, contracts, and evaluation harness, the 32-problem margin cannot be audited for contract difficulty, encoding bias, or solver-friendly formulation.
  2. §V.A.2 and Table I: Code2Inv, CLN2INV, and G-CLN are single-loop designs that the authors ‘extend’ to multi-loop settings, but the paper does not specify the extension protocol (whether they receive LCG-style hierarchical contexts, sequential local contracts only, or independent per-loop runs). If the extensions lack comparable inter-loop context while InvWeaver is given full LCG obligations, the multi-loop gap partly measures protocol asymmetry rather than method strength; a precise, re-runnable multi-loop baseline protocol is needed for the load-bearing comparison.
  3. §IV.A–IV.D and the delayed-filtering rule (§IV.D): LCG construction (how Est/Evd edges are extracted from AST/CFG, how nested back-edges bind provability to outer preservation) and the cycle-length discard threshold are described at a high level without algorithms, edge-label examples beyond the bubble-sort sketch, or sensitivity analysis. Because repair localization and multi-step propagation are the claimed mechanism for the multi-loop gains, these details are load-bearing for both soundness of the method and reproducibility of the refinement path that produces I7/I8-style clauses.
minor comments (6)
  1. Abstract vs. body: abstract says ‘72 out of 82’ without the ‘at least 32 more than strongest competitor’ detail that appears in the introduction; align the abstract with Table I’s competitor margin for consistency.
  2. Figure 1 is dense (five phases + LCG legend); a small worked LCG for Listing 1 with explicit Est/Evd edges would make §IV.A much easier to follow.
  3. §V.A.4: LLM names (Qwen3.7-Max, DeepSeek-V4-Pro, GPT-5.5) and fixed temperature/penalty=0 should be accompanied by model versions/API dates and a note on whether decoding is deterministic across runs.
  4. Efficiency metrics (avg. proposals/time) are reported only on solved instances; stating failure timeouts and unsolved-case cost would clarify the practical overhead of iterative WP refinement.
  5. §VI correctly scopes away dynamic allocation and separation logic; a short quantitative note on how many CLRS-Alg programs were excluded for this reason would help readers bound external validity.
  6. Minor polish: ‘INVWEAVERon’ spacing/typos in the abstract/intro, and consistent capitalization of InvWeaver vs. INVWEAVER.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: empirical multi-loop gains are measured by independent SMT discharge of fixed ACSL contracts, not by construction from fitted inputs or self-justifying definitions.

full rationale

InvWeaver's derivation chain is a standard neuro-symbolic pipeline (LCG abstraction from AST/CFG, obligation-guided LLM prompts, Frama-C WP targets, delayed filtering, re-validation). Success is defined externally by whether Alt-Ergo/Z3/CVC5 discharge the three classical Hoare obligations (establishment, preservation, provability) against author-supplied but fixed ACSL contracts; nothing is fitted to the target metric and then re-reported as a prediction. Self-citations to LaM4Inv and Clause2Inv appear only as baselines or related work and do not supply a uniqueness theorem, ansatz, or load-bearing premise that forces the 72/82 result. The newly curated CLRS-Alg suite and author-side multi-loop extensions of single-loop baselines raise reproducibility questions but do not make the claimed performance circular by the paper's own equations or definitions. Score 1 reflects only the ordinary presence of overlapping-author citations that are not load-bearing.

Assumptions & free parameters 3 free parameters · 5 assumptions · 2 invented entities

The central empirical claim rests on classical Hoare/WP semantics, the soundness of Frama-C WP and SMT solvers, the adequacy of the LCG abstraction for inter-loop proof dependencies, and the ability of frontier LLMs to follow the structured prompts. No numerical free parameters are fitted to the success metric; the main invented construct is the LCG itself as an engineering abstraction rather than a new physical entity.

free parameters (3)
  • SMT solver timeout per query = 10 s
    Fixed at 10 seconds; affects which obligations are treated as failures versus timeouts and therefore which refinements fire.
  • Delayed-filtering threshold = longest cycle length in LCG
    Discard after refinement attempts exceed the longest LCG cycle containing the node; a hand-chosen policy that trades completeness for efficiency.
  • LLM decoding settings = temperature=0, penalty=0
    temperature and penalty set to zero; still leaves model choice and nondeterminism as free experimental knobs.
assumptions (5)
  • standard math Classical Hoare loop rule: establishment, preservation, and (I ∧ ¬B) ⇒ Q suffice for partial correctness of while-loops.
    Stated in §II.A as the definition of a valid loop invariant.
  • standard math Dijkstra weakest-precondition calculus correctly characterizes the weakest condition guaranteeing a postcondition after a statement.
    Used as the deductive backbone for failure diagnosis and repair targets (§II.B, §IV.C).
  • domain assumption Frama-C WP plugin plus Alt-Ergo/Z3/CVC5 can soundly discharge ACSL proof obligations when they succeed within timeout.
    All validation and success metrics depend on this toolchain (§V.A.4).
  • ad hoc to paper The loop-level call graph (state-transition edges plus verification-dependency edges) adequately exposes the inter-loop proof contexts needed for multi-loop invariant synthesis.
    Core design claim of §IV.A; not independently proven, only motivated and evaluated empirically.
  • domain assumption Frontier LLMs can generate and refine ACSL invariants when given structured assumption/obligation contexts and WP targets.
    Neural side of the neuro-symbolic loop; assumed throughout §IV.B–D and ablations.
invented entities (2)
  • Loop-level call graph (LCG)
    purpose: Abstract multi-loop programs into nodes (loops/boundaries) and two edge kinds so that obligations and repairs can be scheduled and propagated.
    Primary structural invention of the paper; independent_evidence is only the empirical success of the pipeline built on it.
  • CLRS-Alg multi-loop benchmark suite
    purpose: Provide harder, algorithmically realistic multi-loop invariant tasks beyond numerical SV-COMP/OOPSLA programs.
    Author-curated dataset of 85 formalized CLRS algorithms/exercises; not an external standard yet.

how reviews work

0 comments
Cite this review

Pith. "Pith review of InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs." pith.science (2026). https://pith.science/paper/IYRREW2V

@misc{pith2026260705478,
  author       = {Pith},
  title        = {Pith review of: InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IYRREW2V}},
  note         = {Machine review of arXiv:2607.05478}
}
read the original abstract

Loop invariant inference is a fundamental yet challenging problem in program verification. Recent LLM-aided guess-and-check techniques have shown strong performance on single-loop programs, but they often struggle with programs containing multiple interacting loops. This paper presents InvWeaver, a neuro-symbolic framework for synthesizing invariants for such programs. The key idea is to expose inter-loop dependencies and propagate proof obligations through a combination of loop-level abstraction, obligation-guided inference, and weakest-precondition-based refinement. We evaluate InvWeaver on a comprehensive benchmark suite, including a newly curated dataset derived from classic algorithms. Experimental results show that InvWeaver substantially outperforms existing invariant inference methods, solving 72 out of 82 multi-loop benchmark problems and maintaining strong performance on single-loop tasks.

Figures

Figures reproduced from arXiv: 2607.05478 by the authors.

Figure 1
Figure 1. Overview of INVWEAVER 2) Obligation-guided inference. INVWEAVER then traverses the LCG top-down for nested loops and boundary-inward for sequential loops, using dependency-relevant specifica￾tions as local proof contexts to prompt initial invariants. 3) Formal validation. A verifier checks the three properties of establishment, preservation, and provability, either pass￾ing the validation or returning the failed inv… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

52 extracted references · 2 canonical work pages

  1. [1]

    Horn-ice learning for synthesizing invariants and contracts,

    P. Ezudheen, D. Neider, D. D’Souza, P. Garg, and P. Madhusudan, “Horn-ice learning for synthesizing invariants and contracts,”Proceed- ings of the ACM on Programming Languages, vol. 2, no. OOPSLA, pp. 1–25, 2018

    2018

  2. [2]

    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,”ACM Sigplan Notices, vol. 51, no. 1, pp. 499–512, 2016

    2016

  3. [3]

    Interval counterexamples for loop invariant learning,

    R. Xu, F. He, and B.-Y . Wang, “Interval counterexamples for loop invariant learning,” inProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2020, pp. 111–122

    2020

  4. [4]

    Learning loop invariants for program verification,

    X. Si, H. Dai, M. Raghothaman, M. Naik, and L. Song, “Learning loop invariants for program verification,”Advances in Neural Information Processing Systems (NeurIPS), vol. 31, 2018

    2018

  5. [5]

    Loop invariant inference through smt solving enhanced reinforcement learning,

    S. Yu, T. Wang, and J. Wang, “Loop invariant inference through smt solving enhanced reinforcement learning,” inProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2023, pp. 175–187

    2023

  6. [6]

    Cln2inv: Learning loop invariants with continuous logic networks,

    G. Ryan, J. Wong, J. Yao, R. Gu, and S. Jana, “Cln2inv: Learning loop invariants with continuous logic networks,” inInternational Conference on Learning Representations (ICLR), 2020

    2020

  7. [7]

    Learning nonlinear loop invariants with gated continuous logic networks,

    J. Yao, G. Ryan, J. Wong, S. Jana, and R. Gu, “Learning nonlinear loop invariants with gated continuous logic networks,” inProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2020, pp. 106–120

    2020

  8. [8]

    Finding in- ductive loop invariants using large language models,

    A. Kamath, A. Senthilnathan, S. Chakraborty, P. Deligiannis, S. K. Lahiri, A. Lal, A. Rastogi, S. Roy, and R. Sharma, “Finding in- ductive loop invariants using large language models,”arXiv preprint arXiv:2311.07948, 2023

    arXiv 2023

Show all 52 references
  1. [9]

    Ranking LLM-generated loop invariants for program verification,

    S. Chakraborty, S. Lahiri, S. Fakhoury, A. Lal, M. Musuvathi, A. Rastogi, A. Senthilnathan, R. Sharma, and N. Swamy, “Ranking LLM-generated loop invariants for program verification,” inFindings of the Association for Computational Linguistics: EMNLP 2023, H. Bouamor, J. Pino, ...

    2023

  2. [10]

    Towards general loop invariant generation: a benchmark of programs with memory manipula- tion,

    C. Liu, X. Wu, Y . Feng, Q. Cao, and J. Yan, “Towards general loop invariant generation: a benchmark of programs with memory manipula- tion,”Advances in Neural Information Processing Systems, vol. 37, pp. 129 120–129 145, 2024

    2024

  3. [11]

    Lemur: Integrating large language models in automated program verification,

    H. Wu, C. Barrett, and N. Narodytska, “Lemur: Integrating large language models in automated program verification,” inThe Twelfth International Conference on Learning Representations (ICLR), 2024

    2024

  4. [12]

    Progress on software verification: Sv-comp 2022,

    D. Beyer, “Progress on software verification: Sv-comp 2022,” inInter- national Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2022, pp. 375–402

    2022

  5. [13]

    Inductive invariant generation via abductive inference,

    I. Dillig, T. Dillig, B. Li, and K. McMillan, “Inductive invariant generation via abductive inference,”SIGPLAN Not., vol. 48, no. 10, p. 443–456, Oct. 2013. [Online]. Available: https://doi.org/10.1145/ 2544173.2509511

    2013

  6. [14]

    T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein,Introduction to algorithms. MIT press, 2022

    2022

  7. [15]

    Software model checking for people who love automata,

    M. Heizmann, J. Hoenicke, and A. Podelski, “Software model checking for people who love automata,” inInternational Conference on Com- puter Aided Verification. Springer, 2013, pp. 36–52

    2013

  8. [16]

    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, 2024, pp. 406–417

    2024

  9. [17]

    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,” inInternational Conference on Computer Aided Verification. Springer, 2024, pp. 302– 328

    2024

  10. [18]

    Z3: An efficient smt solver,

    L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” inInter- national conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337–340

    2008

  11. [19]

    E. W. Dijkstra,A discipline of programming. prentice-hall Englewood Cliffs, 1976, vol. 613924118

    1976

  12. [20]

    Frama-c: A software analysis perspective,

    P. Cuoq, F. Kirchner, N. Kosmatov, V . Prevosto, J. Signoles, and B. Yakobowski, “Frama-c: A software analysis perspective,” inIn- ternational conference on software engineering and formal methods. Springer, 2012, pp. 233–247

    2012

  13. [21]

    Behavioral interface specification languages,

    J. Hatcliff, G. T. Leavens, K. R. M. Leino, P. M ¨uller, and M. Parkinson, “Behavioral interface specification languages,”ACM Computing Surveys (CSUR), vol. 44, no. 3, pp. 1–58, 2012

    2012

  14. [22]

    Enhancing automated loop invariant generation for complex programs with large language models,

    R. Liu, M. Chen, L.-I. Wu, J. Ke, and G. Li, “Enhancing automated loop invariant generation for complex programs with large language models,” Science of Computer Programming, p. 103387, 2025

    2025

  15. [24]

    Qwen3.7: The agent frontier,

    Qwen Team, “Qwen3.7: The agent frontier,” May 2026. [Online]. Available: https://qwen.ai/blog?id=qwen3.7

    2026

  16. [25]

    Deepseek-v4: Towards highly efficient million- token context intelligence,

    A. Xu, B. Lin, B. Xue, B. Wang, B. Xu, B. Wu, B. Zhang, C. Lin, C. Dong, C. Linget al., “Deepseek-v4: Towards highly efficient million- token context intelligence,”arXiv preprint arXiv:2606.19348, 2026

    2026

  17. [26]

    Openai gpt-5 system card,

    A. Singh, A. Fry, A. Perelman, A. Tart, A. Ganesh, A. El-Kishky, A. McLaughlin, A. Low, A. Ostrow, A. Ananthramet al., “Openai gpt-5 system card,”arXiv preprint arXiv:2601.03267, 2025

    2025 arXiv

  18. [27]

    Alt-ergo 2.2,

    S. Conchon, A. Coquereau, M. Iguernlala, and A. Mebsout, “Alt-ergo 2.2,” inSMT Workshop: International Workshop on Satisfiability Modulo Theories, 2018

    2018

  19. [28]

    cvc5: A versatile and industrial-strength smt solver,

    H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. N ¨otzliet al., “cvc5: A versatile and industrial-strength smt solver,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Sp...

    2022

  20. [29]

    Ghosts for lists: a critical module of contiki verified in frama-c,

    A. Blanchard, N. Kosmatov, and F. Loulergue, “Ghosts for lists: a critical module of contiki verified in frama-c,” inNASA Formal Methods Symposium. Springer, 2018, pp. 37–53

    2018

  21. [30]

    Logic against ghosts: Comparison of two proof approaches for a list module,

    ——, “Logic against ghosts: Comparison of two proof approaches for a list module,” inProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, 2019, pp. 2186–2195

    2019

  22. [31]

    The daikon system for dynamic detection of likely invariants,

    M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao, “The daikon system for dynamic detection of likely invariants,”Science of computer programming, vol. 69, no. 1-3, pp. 35–45, 2007

    2007

  23. [32]

    A data driven approach for algebraic loop invariants,

    R. Sharma, S. Gupta, B. Hariharan, A. Aiken, P. Liang, and A. V . Nori, “A data driven approach for algebraic loop invariants,” inEuropean Symposium on Programming. Springer, 2013, pp. 574–592

    2013

  24. [33]

    Dig: A dynamic invariant generator for polynomial and array invariants,

    T. Nguyen, D. Kapur, W. Weimer, and S. Forrest, “Dig: A dynamic invariant generator for polynomial and array invariants,”ACM Trans- actions on Software Engineering and Methodology (TOSEM), vol. 23, no. 4, pp. 1–30, 2014

    2014

  25. [34]

    Bi-abductive resource invariant synthesis,

    C. Calcagno, D. Distefano, and V . Vafeiadis, “Bi-abductive resource invariant synthesis,” inProceedings of the 7th Asian Symposium on Programming Languages and Systems, ser. APLAS ’09. Berlin, Heidelberg: Springer-Verlag, 2009, p. 259–274. [Online]. Available: https://doi.org...

    2009 doi

  26. [35]

    Linear invariant generation using non-linear constraint solving,

    M. A. Col ´on, S. Sankaranarayanan, and H. B. Sipma, “Linear invariant generation using non-linear constraint solving,” inInternational Con- ference on Computer Aided Verification (CAV). Springer, 2003, pp. 420–432

    2003

  27. [36]

    From tests to proofs,

    A. Gupta, R. Majumdar, and A. Rybalchenko, “From tests to proofs,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2009, pp. 262–276

    2009

  28. [37]

    Automatic discovery of linear restraints among variables of a program,

    P. Cousot and N. Halbwachs, “Automatic discovery of linear restraints among variables of a program,” inProceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, ser. POPL ’78. New York, NY , USA: Association for Computing Machinery, 1978, p. 8...

    1978 doi

  29. [38]

    Systematic design of program analysis frameworks,

    P. Cousot and R. Cousot, “Systematic design of program analysis frameworks,” inProceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, ser. POPL ’79. New York, NY , USA: Association for Computing Machinery, 1979, p. 269–282. [Online]. Availa...

    1979 doi

  30. [39]

    Affine relationships among variables of a program,

    M. Karr, “Affine relationships among variables of a program,”Acta Informatica, vol. 6, no. 2, pp. 133–151, 1976

    1976

  31. [40]

    The eldarica horn solver,

    H. Hojjat and P. R ¨ummer, “The eldarica horn solver,” in2018 Formal Methods in Computer Aided Design (FMCAD). IEEE, 2018, pp. 1–7

    2018

  32. [41]

    Global guidance for local generalization in model checking,

    H. G. Vediramana Krishnan, Y . Chen, S. Shoham, and A. Gurfinkel, “Global guidance for local generalization in model checking,”Formal Methods in System Design, vol. 63, no. 1, pp. 81–109, 2024

    2024

  33. [42]

    A practical and complete approach to predicate refinement,

    R. Jhala and K. L. McMillan, “A practical and complete approach to predicate refinement,” inProceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, ser. TACAS’06. Berlin, Heidelberg: Springer-Verlag, 2006, p. 459–4...

    2006 doi

  34. [43]

    Lazy annotation for program testing and verification,

    K. L. McMillan, “Lazy annotation for program testing and verification,” inProceedings of the 22nd International Conference on Computer Aided Verification, ser. CA V’10. Berlin, Heidelberg: Springer- Verlag, 2010, p. 104–118. [Online]. Available: https://doi.org/10.1007/ 978-3-...

    2010

  35. [44]

    Barrett, C

    C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi ´c, T. King, A. Reynolds, and C. Tinelli, “Cvc4,” inProceedings of the 23rd International Conference on Computer Aided Verification, ser. CA V’11. Berlin, Heidelberg: Springer-Verlag, 2011, p. 171–177

    2011

  36. [45]

    Data-driven precondition infer- ence with learned features,

    S. Padhi, R. Sharma, and T. Millstein, “Data-driven precondition infer- ence with learned features,”ACM SIGPLAN Notices, vol. 51, no. 6, pp. 42–56, 2016

    2016

  37. [46]

    Ice: A robust framework for learning invariants,

    P. Garg, C. L ¨oding, P. Madhusudan, and D. Neider, “Ice: A robust framework for learning invariants,” inInternational Conference on Computer Aided Verification (CAV). Springer, 2014, pp. 69–87

    2014

  38. [47]

    Multi-phase invariant synthesis,

    D. Riley and G. Fedyukovich, “Multi-phase invariant synthesis,” in Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ser. ESEC/FSE 2022. New York, NY , USA: Association for Computing Machinery, ...

    2022 doi

  39. [48]

    Interpolants as classifiers,

    R. Sharma, A. V . Nori, and A. Aiken, “Interpolants as classifiers,” in Proceedings of the 24th International Conference on Computer Aided Verification, ser. CA V’12. Berlin, Heidelberg: Springer-Verlag, 2012, p. 71–87. [Online]. Available: https://doi.org/10.1007/978-3-642-31424-7 11

    2012 doi

  40. [49]

    Automatic loop- invariant generation anc refinement through selective sampling,

    J. Li, J. Sun, L. Li, Q. L. Le, and S.-W. Lin, “Automatic loop- invariant generation anc refinement through selective sampling,” in 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2017, pp. 782–792

    2017

  41. [50]

    Verification as learning geometric concepts,

    R. Sharma, S. Gupta, B. Hariharan, A. Aiken, and A. V . Nori, “Verification as learning geometric concepts,” inStatic Analysis: 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22,

    2013

  42. [51]

    Springer, 2013, pp

    Proceedings 20. Springer, 2013, pp. 388–411

    2013

  43. [52]

    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,” Proceedings of the ACM on Software Engineering, vol. 2, no. ISSTA, pp. 1009–1030, 2025

    2025

  44. [53]

    Integrating symbolic execution with llms for automated generation of program specifications,

    F. Yang, X. Ma, S. Wang, X. Xu, Q. Cao, N. Zhan, X. Li, and B. Gu, “Integrating symbolic execution with llms for automated generation of program specifications,” 2026. [Online]. Available: https://arxiv.org/abs/2506.09550

    2026

Pith tools

Reviewed July 11, 2026 · model on record in the stance chip above.