Path-Sensitive Loop Invariant Inference via Large Language Models and Abstract Interpretation
TL;DR
A path-sensitive loop invariant inference approach based on Large Language Models and abstract interpretation that constructs candidate invariants as disjunctions of clause conjunctions satisfied by counterexamples across loop paths and iteratively refines them using counterexamples generated by the SMT solver during verification.
Abstract
Loop invariant inference remains a core challenge in program verification, particularly when disjunctive invariants are required. In this paper, we present a path-sensitive loop invariant inference approach based on Large Language Models (LLMs) and abstract interpretation. We apply abstract interpretation to derive initial invariants, which, if insufficient to verify the program, guide an LLM-based agent to generate more precise, path-specific clauses. The core of our method is Counterexample-Guided Clause Combination (CEGCC), a novel strategy that constructs candidate invariants as disjunctions of clause conjunctions satisfied by counterexamples across loop paths, and iteratively refines them using counterexamples generated by the SMT solver during verification. This shifts the focus of invariant synthesis from blind enumeration to semantic refinement driven by genuine counterexample verification and generation. To further refine this approach, we leverage dependencies across different loop paths, apply abstract interpretation to improve SMT solving, and deploy a second LLM-based agent for counterexample verification and mutation. Results show PAL2Inv matches state-of-the-art LLM methods on linear benchmarks and verifies 53–142% more programs on multi-phase benchmarks, while remaining competitive with specialized symbolic multi-phase verifiers.