# Ilinva: Using Abduction to Generate Loop Invariants

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Jun 2019.

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

- [Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis](https://mlsanity.com/paper/2205.14229/) (2022)
- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [LLM For Loop Invariant Generation and Fixing: How Far Are We?](https://mlsanity.com/paper/2511.06552/) (2025)

## Abstract (arXiv)

We describe a system to prove properties of programs. The key feature of this approach is a method to automatically synthesize inductive invariants of the loops contained in the program. The method is generic, i.e., it applies to a large set of programming languages and application domains; and lazy, in the sense that it only generates invariants that allow one to derive the required properties. It relies on an existing system called GPiD for abductive reasoning modulo theories, and on the platform for program verification Why3. Experiments show evidence of the practical relevance of our approach.