# Ilinva: Using Abduction to Generate Loop Invariants

## TL;DR

Ilinva introduces an automated, generic, and lazy method for synthesizing loop invariants using abductive reasoning, enhancing program verification across diverse languages and domains.

## Contribution

It presents a novel approach combining abductive reasoning with invariant synthesis, integrated into the GPiD system and Why3 platform, for improved program property proofs.

## Key findings

- Effective invariant synthesis demonstrated on various programs
- Applicable to multiple programming languages and domains
- Practical relevance confirmed through experiments

## Abstract

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.