# LoopInvGen: A Loop Invariant Generator based on Precondition Inference

arXiv: https://arxiv.org/abs/1707.02029 · HTML: https://mlsanity.com/paper/1707.02029/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Jul 2017.

## Built on by (most cited first, 3 of 3)

- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Satisfiability and Synthesis Modulo Oracles](https://mlsanity.com/paper/2107.13477/) (2021)
- [LLM For Loop Invariant Generation and Fixing: How Far Are We?](https://mlsanity.com/paper/2511.06552/) (2025)

## Abstract (arXiv)

We describe the LoopInvGen tool for generating loop invariants that can provably guarantee correctness of a program with respect to a given specification. LoopInvGen is an efficient implementation of the inference technique originally proposed in our earlier work on PIE (https://doi.org/10.1145/2908080.2908099). In contrast to existing techniques, LoopInvGen is not restricted to a fixed set of features -- atomic predicates that are composed together to build complex loop invariants. Instead, we start with no initial features, and use program synthesis techniques to grow the set on demand. This not only enables a less onerous and more expressive approach, but also appears to be significantly faster than the existing tools over the SyGuS-COMP 2018 benchmarks from the INV track.