Pith. sign in

REVIEW 3 major objections 5 minor 44 references

Loop invariants are best learned as ordered sequences of relatively inductive lemmas, and this decomposition lets LimICE solve 349/367 linear and 47/50 nonlinear benchmarks while running 36-63% faster than prior LLM-based methods.

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 ↗

T0 review · deepseek-v4-flash

2026-08-01 04:43 UTC pith:XTEAX3NO

load-bearing objection The incremental-ICE formal core is sound and the evaluation is thoughtful, but the headline empirical claim currently rests on an unshipped, curated benchmark suite, so treat the 349/367 and 47/50 numbers as conditional until the artifacts appear. the 3 major comments →

arxiv 2607.27606 v1 pith:XTEAX3NO submitted 2026-07-30 cs.SE

LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference

Kai Fan , ShiWen Yu , GuangSheng Fan , HaoAng Chi , WanWei Liu , Ji Wang This is my paper
classification cs.SE
keywords loop invariant synthesisICE frameworkincremental learningIC3large language modelsprogram verificationlemma sequencecounterexample filtering
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.

This paper argues that the conventional approach to learning loop invariants—proposing one complete formula in a single shot—is the wrong target. The authors observe that in practice an invariant is typically an ordered conjunction of simpler lemmas, where later lemmas are inductive only relative to earlier ones. They extend the ICE counterexample-guided learning framework into Incremental ICE by adding a lemma-specific learning objective and a counterexample filtering rule that keeps the counterexample set from over-constraining later learning steps. The instantiated tool, LimICE, uses a large language model to generate atomic literals, a 2-CNF search to assemble candidate lemmas, and a decision-tree learner as a fallback. On 367 linear and 50 nonlinear benchmarks, LimICE solves more instances than eight state-of-the-art baselines and runs faster than the other LLM-based tools. The implication is that decomposing invariant synthesis into an ordered sequence of small learning tasks is not only feasible but empirically advantageous.

Core claim

The central claim is that a loop invariant is rarely a single monolithic formula but an ordered sequence of assertions ψ1,...,ψn, each holding initially and each inductive relative to all its predecessors, together strong enough to imply the postcondition. The paper proves that this structure can be learned incrementally inside the ICE framework: a new candidate lemma needs only to satisfy a lemma-specific objective—true on all positive counterexamples, false on at least one negative counterexample, and preserved across inductive counterexamples given the existing lemmas—and, once a lemma is accepted, the counterexamples it already falsifies can be safely discarded. This filtering is shown t

What carries the argument

The load-bearing mechanism is the lemma-specific learning objective (Equation 3) together with the counterexample filtering rule (Equation 4) inside the Incremental ICE framework. The objective relaxes the monolithic ICE requirement: a new lemma need not alone imply the postcondition; it must only pass all positive counterexamples, reject at least one negative counterexample, and be inductive relative to the already-accepted lemmas. The filtering rule then deletes inductive and negative counterexamples that the new lemma already falsifies, because any future lemma that is a strengthening of the sequence would also falsify them; this prevents the counterexample set from growing without bound

Load-bearing premise

The empirical claim that LimICE outperforms the baselines rests on the curated benchmark suite being a neutral and unseen testbed for the LLM; if the large language model used has memorized these public programs' invariants during pretraining, the reported advantage would be overstated.

What would settle it

Take a set of programs equivalent in structure to the public benchmarks but with variable names, constants, and loop bounds randomly permuted so that the LLM cannot pattern-match any memorized solution, then re-run LimICE and the strongest baselines on this fresh suite and compare solved counts and runtimes. If the margin shrinks to a few instances or reverses, the original advantage is due to benchmark memorization rather than the incremental framework.

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

If this is right

  • If the central claim holds, invariant synthesis tools can replace monolithic LLM prompting with a structured decomposition into lemma-learning steps, improving both convergence and reuse of intermediate results.
  • The counterexample filtering rule means the learner never needs to reason over counterexamples that are already ruled out by accepted lemmas, so the search space stays small and the method scales to harder benchmarks.
  • Because the lemma sequence exposes proof progress, it can be fed back into the LLM as a 'reason generation' prompt, which the paper shows solves more instances than random literal generation alone.
  • The framework is orthogonal to existing LLM-based invariant generators: the paper notes it can be combined with re-ranking and fine-tuning techniques, so future gains in LLM literal generation should transfer directly to LimICE.
  • A fallback to precise decision-tree learning (ICE-DT) makes the overall tool less dependent on LLM capability, preserving strong performance even with a 7B-parameter model.

Where Pith is reading between the lines

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

  • Our inference: the same incremental ICE structure could be applied to other counterexample-guided synthesis tasks beyond loop invariants—e.g., ranking functions for termination or heap abstractions—wherever a monolithic hypothesis over-constrains learning.
  • Our inference: the reason-generation prompt exploits the lemma sequence as a communication channel between the search state and the LLM. One could push this further by using the SMT-based failure proof as a feedback signal to the model in-context, turning LimICE into a closed-loop repair system, which the paper does not explore.
  • Our inference: because the empirical advantage depends on the public benchmark suite, a clean test of generality would be to regenerate benchmarks with perturbed constants and variable names after the LLM's training cutoff; if the advantage persists, the incremental mechanism itself is the source of the gains rather than memorization.

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 proposes Incremental ICE, an extension of the ICE learning framework that synthesizes loop invariants as an ordered sequence of lemmas rather than a single monolithic formula. The framework introduces a lemma-specific learning objective and a counterexample-filtering mechanism, and the authors prove the filtering rule to be sound. The paper instantiates the framework in LimICE, which uses an LLM (DeepSeek V3.2) to generate candidate literals, a 2-CNF search to combine them into lemmas, and ICE-DT as a fallback synthesizer. The evaluation compares LimICE with eight baselines on 367 linear and 50 nonlinear benchmarks, reporting superior solved counts and competitive runtimes.

Significance. If the empirical claims are supported, the work is a meaningful contribution: it provides a principled incremental alternative to monolithic invariant synthesis, with a clean formal core and a practical tool. The paper includes useful ablations, a controlled comparison with monolithic combination, and experiments across different LLM backends, which strengthen the evidence. However, the current evaluation is compromised by the absence of the curated benchmark artifact and by unclear statements about whether all baselines were re-run on the same files. The formal soundness of the filtering argument is correct, but the central SOTA claim is not yet verifiable.

major comments (3)
  1. [Section 5.1] The benchmark suite is not available for verification. The text states that existing linear benchmarks received 'correctness-oriented and semantics-preserving refinements' and that 54 CHC-Comp and 20 Clause2Inv examples are new or rewritten, with details 'provided in the supplementary material,' but the arXiv submission contains no supplementary file. The 'Implementations' paragraph that 'All experiments are conducted under identical settings' does not explicitly say that every baseline (LoopInvGen, ICE-DT, ICE-DT-Interval, Code2Inv, CLN2INV, Clause2Inv, LaM4Inv, LIPuS) was re-run on the exact same assembled 367/50 files with the same 600-second timeout. If any Table 1/Table 2 baseline counts are taken from earlier papers, they are not directly comparable because the benchmark set differs. Please provide the artifact and a per-baseline protocol statement.
  2. [Section 6] The threats to validity do not discuss the possibility that DeepSeek V3.2 has memorized the public benchmark programs and their expected invariants. The evaluation suite is composed entirely of public instances (Code2Inv, LaM4Inv, CHC-Comp, Clause2Inv), so the LLM may have seen them during pretraining, giving an advantage to LLM-based methods, including LimICE. The QWen2.5-7B experiment does not rule this out because that model may also have been trained on GitHub data. The authors should either evaluate on a private held-out set whose invariants were not public before the model's cutoff date, or present a concrete argument why memorization cannot explain the margin over non-LLM baselines.
  3. [Section 4.2.2] Algorithm 2 is under-specified. The operations `Prohibit(clauseSet, CNF)`, `UnitRefine(CNF, clauseSet)`, and the transfer of elements between `lemmaList` and `reserveSet` are described informally; in particular, the final `reserveSet.append(lemmaList/candidate)` suggests that all remaining candidates are moved to `reserveSet` except the selected candidate, but it is not clear what happens to the refined or prohibited clauses. The termination of the search is not argued (e.g., a well-founded measure on the finite set of clauses and unit refinements). Without a precise specification, the reproducibility of the search and the claimed efficiency are difficult to assess.
minor comments (5)
  1. [Section 3.2] Eq. (4) and (6): the notation '¯𝑥=𝑖1⇒...' is nonstandard; use a substitution or assignment notation for clarity.
  2. [Page 2] The author block contains 'Trovato et al.', which appears to be a template artifact; please update to the correct author list.
  3. [References] Reference [31]: the author name is misspelled as 'Rimmer'; should be 'Rümmer'.
  4. [Table 5 caption] Define 'LimICE-base' and 'Hard' in the caption; currently these are only defined in the body text.
  5. [Section 5.2] In the first paragraph of the nonlinear results, 'Clause2inv' is a typo; should be 'Clause2Inv'.

Circularity Check

0 steps flagged

No significant circularity: Incremental ICE's soundness follows from its definitions; benchmark concerns are external validity, not circularity.

full rationale

The derivation of Incremental ICE is self-contained. Definition 3.1 defines a lemma sequence by initiation, relative inductiveness, and joint sufficiency; the conjunction of such a sequence is a standard inductive invariant, and the paper's lines 13/18 return only after SMT checks Pre/Indu/Post. Equation (3) is the learner objective, and Equation (6) is a propositional tautology: if the new lemma ψ_k is false at i1, then any extension ψ' makes the antecedent of the implication false, so the inductive counterexample (i1,i2) cannot constrain the rest of the sequence; the same holds for negative counterexamples where ψ_k is false. Filtering therefore removes only counterexamples already satisfied by the conjunction, so no future lemma is forced by construction. No parameter is fitted to the benchmark results and renamed a prediction; the empirical comparisons are external measurements. The only self-citation is LIPuS [43] as a baseline, which is not load-bearing for the framework's soundness. The benchmark-curation and missing-supplementary-material issues in Section 5.1 are external-validity/reproducibility threats, not circularity; similarly, LLM memorization of public benchmarks is an empirical risk, not a definitional reduction. Hence no circular step is identified.

Axiom & Free-Parameter Ledger

2 free parameters · 5 axioms · 0 invented entities

The framework introduces no new physical or formal entities in the sense of new particles, forces, or dimensions. The only 'inventions' are algorithmic: the lemma-sequence objective, counterexample filtering, and the hybrid LLM/ICE-DT workflow. These are captured as axioms and free parameters above.

free parameters (2)
  • ICE-DT iterations per round n = 30
    Algorithm 1 takes n; Section 5.1 says 'we set the iteration number of ICE-DT in each iteration to 30.' This is a hand-set hyperparameter, not derived from theory.
  • Maximum iterations for LLM-backend experiments = 50
    Section 5.3: 'this experiment also constrains the maximum number of iterations to 50' in addition to the time limit. This cap can affect which problems are solved, especially for weaker LLMs.
axioms (5)
  • standard math The counterexample-filtering equations (Eq. 4-6) preserve all information needed to learn the final conjunction of lemmas.
    Propositional logic; the paper proves the safety of filtering in Section 3.2. This is a real theorem, not an empirical guess.
  • domain assumption SMT solvers return correct answers for the pre/indu/post checks.
    Section 6 acknowledges SMT solver limitations and cites known soundness bugs; the algorithm treats the SMT solver as an oracle.
  • ad hoc to paper The 2-CNF hypothesis space over LLM-and-warm-start literals is expressive enough for the target invariants.
    Section 4.2.2: 'Our empirical results indicate that 2-CNF combinations of literals generated by the LLM are sufficient to synthesize the majority of loop invariants in the evaluated benchmarks.' This is a load-bearing empirical claim, not a proven bound.
  • domain assumption LLM-generated literals are useful and are not inflated by pretraining on the evaluation benchmarks.
    The evaluation uses public benchmark suites with DeepSeek V3.2; no leakage analysis is reported in Sections 5.1-5.2.
  • domain assumption The modified and newly curated benchmark files are representative and are applied uniformly to all baselines.
    Section 5.1 says existing benchmarks were refined and new CHC-Comp rewrites were added; comparison validity depends on all tools seeing the same corrected files.

pith-pipeline@v1.3.0-daily-deepseek · 18415 in / 12373 out tokens · 141839 ms · 2026-08-01T04:43:51.625347+00:00 · methodology

0 comments
read the original abstract

Loop invariant synthesis is a fundamental problem in program verification, yet the inherent undecidability makes it highly challenging. Recent studies have increasingly employed various machine learning techniques to generate loop invariants. However, most of these methods adopt a monolithic approach. Due to the inability to strictly constrain the learning process, learning-based methods struggle to simultaneously consider all necessary conditions and generate complete invariants when tackling complex problems. In fact, a loop invariant is often an ordered sequence of lemmas, rather than a single invariant formula. This motivates us to propose Incremental ICE, a novel learning framework for incremental synthesis. Our framework integrates the incremental philosophy of IC3 into the general invariant learning framework ICE. By defining a lemma-specific learning objective and introducing a counterexample filtering mechanism, we can achieve sound incremental learning. Under this framework, we instantiate a loop invariant synthesis tool, LimICE, which leverages LLMs to generate the ordered sequence of lemmas and incorporates ICE-DT as a fallback mechanism to complement the lemma sequence. Experiments on 367 linear benchmarks and 50 nonlinear benchmarks demonstrate the effectiveness of the proposed approach. LimICE solves 349 (out of 367) linear problems on an average of 15.2 seconds and 47 (out of 50) nonlinear problems on an average of 8.8 seconds. Compared to the state-of-the-art LLM-based baseline, our approach solves 12-24% more instances while running 36-63% faster across linear and nonlinear benchmarks. LimICE also consistently outperforms strong non-LLM baselines and solves at least 86 and 27 additional instances on the linear and nonlinear benchmarks, respectively.

Figures

Figures reproduced from arXiv: 2607.27606 by GuangSheng Fan, Haoang Chi, Ji Wang, Kai Fan, Shiwen Yu, Wanwei Liu.

Figure 1
Figure 1. Figure 1: Comparison between the Incremental ICE framework and the Original ICE framework. [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A Framework of LimICE. learning process, while Modules M3 and M4 together form the fallback learning process. The remainder of this section first presents an overview of LimICE, followed by the details of its core components. 4.1 The Overall Algorithm The overall algorithm of LimICE is summarized in Algorithm 1. Given the program, LimICE first initializes the data structures and performs a warm start on th… view at source ↗
Figure 3
Figure 3. Figure 3: A complex benchmark of cast study 1. The complete invariant is complex, and when the problem is solved, the number of cumulative literals generated by LLM and warm start has reached 91. Finding such an invariant in the vast combinatorial space is difficult. However, LimICE adopts an incremental approach; it discovers seven relatively simple lemmas during the synthesis process rather than trying to obtain t… view at source ↗
Figure 4
Figure 4. Figure 4: A complex benchmark of cast study 2. LimICE first synthesizes the following five lemmas: (1) 𝑥 ≥ 0 ∨ 𝑥 = 0 (4) (𝑥 + 𝑦 = 10 ∨ 𝑥 = 𝑦) ∧ (𝑥 + 𝑦 = 10 ∨ 𝑥 = 0) (2) 𝑥 ≤ 9 (5) 𝑧 ≤ 10 − (𝑦 − 𝑥) ∨ 𝑥 = 𝑦 (3) 𝑦 ≥ 0 . J. ACM, Vol. 37, No. 4, Article 111. Publication date: August 2018 [PITH_FULL_IMAGE:figures/full_fig_p017_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

44 extracted references · 3 linked inside Pith

  1. [1]

    Mostafijur Rahman Akhond, Saikat Chakraborty, and Gias Uddin. 2025. LLM For Loop Invariant Generation and Fixing: How Far Are We?arXiv preprint arXiv:2511.06552(2025)

    arXiv 2025

  2. [2]

    Ahmed Bouajjani, Wael-Amine Boutglay, and Peter Habermehl. 2025. Data-driven verification of procedural programs with integer arrays. InInternational Conference on Computer Aided Verification. Springer, 338–363

    2025

  3. [3]

    Aaron R Bradley. 2011. SAT-based model checking without unrolling. InInternational Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 70–87

    2011

  4. [4]

    Aaron R Bradley. 2012. Understanding ic3. InInternational Conference on Theory and Applications of Satisfiability Testing. Springer, 1–14

    2012

  5. [5]

    Weining Cao, Guangyuan Wu, Tangzhi Xu, Yuan Yao, Hengfeng Wei, Taolue Chen, and Xiaoxing Ma. 2025. Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference.Proceedings of the ACM on Software Engineering 2, ISSTA (2025), 1009–1030

    2025

  6. [6]

    Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Akash Lal, Madanlal Musuvathi, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, and Nikhil Swamy. 2023. Ranking llm-generated loop invariants for program verification. InFindings of the Association for Computational Linguistics: EMNLP 2023. 9164–9175

    2023

  7. [7]

    Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InProceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 238–252

    1977

  8. [8]

    Patrick Cousot and Nicolas Halbwachs. 1978. Automatic discovery of linear restraints among variables of a program. InProceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 84–96

    1978

  9. [9]

    Christoph Csallner, Nikolai Tillmann, and Yannis Smaragdakis. 2008. DySy: Dynamic symbolic execution for invariant inference. InProceedings of the 30th international conference on Software engineering. 281–290

    2008

  10. [10]

    Isil Dillig, Thomas Dillig, Boyang Li, and Ken McMillan. 2013. Inductive invariant generation via abductive inference. Acm Sigplan Notices48, 10 (2013), 443–456

    2013

  11. [11]

    Mnacho Echenim, Nicolas Peltier, and Yanis Sellami. 2019. Ilinva: Using abduction to generate loop invariants. In International Symposium on Frontiers of Combining Systems. Springer, 77–93

    2019

  12. [12]

    Michael D Ernst, Jake Cockrell, William G Griswold, and David Notkin. 2001. Dynamically discovering likely program invariants to support program evolution.IEEE transactions on software engineering27, 2 (2001), 99–123

    2001

  13. [13]

    P Ezudheen, Daniel Neider, Deepak D’Souza, Pranav Garg, and P Madhusudan. 2018. Horn-ICE learning for synthesizing invariants and contracts.Proceedings of the ACM on Programming Languages2, OOPSLA (2018), 1–25

    2018

  14. [14]

    Robert W Floyd. 1993. Assigning meanings to programs. InProgram Verification: Fundamental Issues in Computer Science. Springer, 65–81

    1993

  15. [15]

    Carlo A Furia, Bertrand Meyer, and Sergey Velder. 2014. Loop invariants: Analysis, classification, and examples.ACM Computing Surveys (CSUR)46, 3 (2014), 1–51

    2014

  16. [16]

    Pranav Garg, Christof Löding, Parthasarathy Madhusudan, and Daniel Neider. 2014. ICE: A robust framework for learning invariants. InInternational Conference on Computer Aided Verification. Springer, 69–87

    2014

  17. [17]

    Pranav Garg, Daniel Neider, Parthasarathy Madhusudan, and Dan Roth. 2016. Learning invariants using decision trees and implication counterexamples.ACM Sigplan Notices51, 1 (2016), 499–512

    2016

  18. [18]

    Ashutosh Gupta, Rupak Majumdar, and Andrey Rybalchenko. 2009. From tests to proofs. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 262–276

    2009

  19. [19]

    Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming.Commun. ACM12, 10 (1969), 576–580. J. ACM, Vol. 37, No. 4, Article 111. Publication date: August 2018. 111:20 Trovato et al

    1969

  20. [20]

    Hossein Hojjat and Philipp Rümmer. 2018. The ELDARICA horn solver. In2018 Formal Methods in Computer Aided Design (FMCAD). IEEE, 1–7

    2018

  21. [21]

    Ranjit Jhala and Kenneth L McMillan. 2006. A practical and complete approach to predicate refinement. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 459–473

    2006

  22. [22]

    Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. 2023. Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948(2023)

    Pith/arXiv arXiv 2023

  23. [23]

    Chang Liu, Xiwei Wu, Yuan Feng, Qinxiang Cao, and Junchi Yan. 2024. Towards general loop invariant generation: a benchmark of programs with memory manipulation.Advances in Neural Information Processing Systems37 (2024), 129120–129145

    2024

  24. [24]

    2012.Temporal verification of reactive systems: safety

    Zohar Manna and Amir Pnueli. 2012.Temporal verification of reactive systems: safety. Springer Science & Business Media

    2012

  25. [25]

    Kenneth L McMillan. 2010. Lazy annotation for program testing and verification. InInternational Conference on Computer Aided Verification. Springer, 104–118

    2010

  26. [26]

    ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. 2012. Using dynamic analysis to discover polynomial and array invariants. In2012 34th International Conference on Software Engineering (ICSE). IEEE, 683–693

    2012

  27. [27]

    Saswat Padhi, Rahul Sharma, and Todd Millstein. 2016. Data-driven precondition inference with learned features. ACM SIGPLAN Notices51, 6 (2016), 42–56

    2016

  28. [28]

    Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. 2023. Can large language models reason about program invariants?. InInternational Conference on Machine Learning. PMLR, 27496–27520

    2023

  29. [29]

    Muhammad AA Pirzada, Giles Reger, Ahmed Bhayat, and Lucas C Cordeiro. 2024. Llm-generated invariants for bounded model checking without loop unrolling. InProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. 1395–1407

    2024

  30. [30]

    Daniel Riley and Grigory Fedyukovich. 2022. Multi-phase invariant synthesis. InProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 607–619

    2022

  31. [31]

    2025.aeval-benchmarks

    Philipp Rimmer. 2025.aeval-benchmarks. https://github.com/chc-comp/aeval-benchmarks Accessed: 2025

    2025

  32. [32]

    Enric Rodríguez-Carbonell and Deepak Kapur. 2004. Program verification using automatic generation of invariants. In International Colloquium on Theoretical Aspects of Computing. Springer, 325–340

    2004

  33. [33]

    Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. 2019. CLN2INV: learning loop invariants with continuous logic networks.arXiv preprint arXiv:1909.11542(2019)

    Pith/arXiv arXiv 2019

  34. [34]

    Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. 2018. Learning loop invariants for program verification.Advances in Neural Information Processing Systems31 (2018)

    2018

  35. [35]

    Constraint Solving. 2003. Linear Invariant Generation Using Non-linear.Computer-aided Verification: Proceedings (2003), 420

    2003

  36. [36]

    Fabio Somenzi and Aaron R Bradley. 2011. IC3: where monolithic and incremental meet. In2011 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 3–8

    2011

  37. [37]

    Hari Govind Vediramana Krishnan, YuTing Chen, Sharon Shoham, and Arie Gurfinkel. 2024. Global guidance for local generalization in model checking.Formal Methods in System Design63, 1 (2024), 81–109

    2024

  38. [38]

    Dominik Winterer, Chengyu Zhang, and Zhendong Su. 2020. Validating SMT solvers via semantic fusion. InProceedings of the 41st ACM SIGPLAN Conference on programming language design and implementation. 718–730

    2020

  39. [39]

    Guangyuan Wu, Weining Cao, Yuan Yao, Hengfeng Wei, Taolue Chen, and Xiaoxing Ma. 2024. Llm meets bounded model checking: Neuro-symbolic loop invariant inference. InProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. 406–417

    2024

  40. [40]

    Haoze Wu, Clark Barrett, and Nina Narodytska. 2023. Lemur: Integrating large language models in automated program verification.arXiv preprint arXiv:2310.04870(2023)

    Pith/arXiv arXiv 2023

  41. [41]

    Rongchen Xu, Fei He, and Bow-Yaw Wang. 2020. 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. 111–122

    2020

  42. [42]

    Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu. 2020. Learning nonlinear loop invariants with gated continuous logic networks. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 106–120

    2020

  43. [43]

    Shiwen Yu, Ting Wang, and Ji Wang. 2023. Loop invariant inference through SMT solving enhanced reinforcement learning. InProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis. 175–187

    2023

  44. [44]

    He Zhu, Aditya V Nori, and Suresh Jagannathan. 2015. Learning refinement types.ACM SIGPLAN Notices50, 9 (2015), 400–411. J. ACM, Vol. 37, No. 4, Article 111. Publication date: August 2018

    2015