pith. sign in

arxiv: 1906.11033 · v1 · pith:PEF6K4ZTnew · submitted 2019-06-26 · 💻 cs.LO

Ilinva: Using Abduction to Generate Loop Invariants

Mnacho Echenim , Nicolas Peltier , Yanis Sellami This is my paper

Pith reviewed 2026-05-25 15:20 UTC · model grok-4.3

classification 💻 cs.LO
keywords loop invariantsabductive reasoningprogram verificationinductive invariantsautomated synthesisWhy3
0
0 comments X

The pith

Abduction synthesizes the loop invariants needed to prove program properties.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper describes a system that automatically generates inductive invariants for loops inside programs. It does so by using abduction to produce only those invariants that let one derive the properties one actually wants to prove. The method is built to work with many different programming languages and problem domains. It combines an existing abductive reasoner called GPiD with the Why3 verification platform, and the authors report that experiments support its usefulness on practical examples.

Core claim

The Ilinva system automatically synthesizes inductive invariants of the loops contained in the program by relying on abductive reasoning modulo theories, and does so in a lazy manner so that only invariants allowing one to derive the required properties are generated.

What carries the argument

Abductive reasoning modulo theories performed by GPiD to produce invariants sufficient to discharge verification conditions generated by Why3.

Load-bearing premise

The abductive reasoning provided by GPiD will produce invariants sufficient to discharge the verification conditions generated by Why3 for a wide range of practical programs and theories without requiring extensive manual tuning.

What would settle it

A benchmark program for which the invariants returned by the abduction procedure still leave some verification conditions unprovable inside Why3.

Figures

Figures reproduced from arXiv: 1906.11033 by Mnacho Echenim, Nicolas Peltier, Yanis Sellami.

Figure 1
Figure 1. Figure 1: A simple program on lists It contains one loop for which we will generate an invariant. A location is a finite sequence of natural numbers. The empty location is denoted by ε and the concatenation of two locations ℓ and ℓ ′ is denoted by ℓ.ℓ′ . If ℓ is a location and S is a set of locations then ℓ.S denotes the set {ℓ.ℓ′ | ℓ ′ ∈ S}. The set of locations in a program P or in an instruction I is in￾ductively… view at source ↗
Figure 2
Figure 2. Figure 2: A Weakest Precondition Calculus sp(φ, empty) = φ sp(φ, I ; P ′ ) = sp(sp(φ, I), P ′ ) sp(φ, assume φ ′ ) = φ ∧ φ ′ sp(φ, assert φ ′ ) = φ sp(φ, if C then P1 else P2) = sp(φ ∧ C, P1) ∨ sp(φ ∧ ¬C, P2) sp(φ, while C do P1{ψ} end) = ψ ∧ ¬C sp(φ, P) describes the state of the memory after P. The conditions corresponding to loops are approximated by using the provided loop invariants (the corresponding veri￾fica… view at source ↗
Figure 3
Figure 3. Figure 3: A Strongest Postcondition Calculus 3. Loop pre-conditions, ensuring that the loop invariants hold when the corre￾sponding loop is entered. Given a loop L occurring at position ℓ in program P, we denote by VCgeninit(P, ℓ) the set of assertions ensuring that the loop invariant holds before loop L is entered. Thus, VCgen(P) = VCgena (P) ∪ S ℓ∈lloc(P) (VCgenind(P, ℓ) ∪ VCgeninit(P, ℓ)) . Such verification co… view at source ↗
Figure 4
Figure 4. Figure 4: Backward and Forward Propagation of Abductive Hypotheses Algorithm 4: Ind (Program P, Location ℓ) 1 if all formulas in VCgenind(P, ℓ) are valid then 2 return P; 3 let φ be a non-valid formula in VCgenind(P, ℓ) ; 4 let Ξ ←− Abduce(φ, P, ℓ); 5 foreach ξ ∈ Ξ do 6 foreach ℓ ′ ∈ lloc(P) such that ℓ is a prefix of ℓ ′ (with possibly ℓ = ℓ ′ ) do 7 let ξ ′ ←− fp(ξ, P, ℓ, ℓ′ ); 8 let P ′ ξ ←− Strengthen(P, ℓ′ , ξ′… view at source ↗
Figure 5
Figure 5. Figure 5: Workflow graph of the Ilinva tool [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Experimental Results [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The paper presents Ilinva, a system for proving program properties by automatically synthesizing inductive loop invariants. The method uses abductive reasoning modulo theories provided by the external GPiD tool and integrates with the Why3 verification platform. It is claimed to be generic (applicable to many languages and domains) and lazy (generating only invariants sufficient to discharge the required verification conditions). Experiments are asserted to demonstrate practical relevance.

Significance. If the central claims hold with supporting data, the work would demonstrate a modular, tool-composed approach to invariant generation that avoids manual invariant crafting while remaining domain-agnostic. The explicit reliance on existing, off-the-shelf components (GPiD and Why3) is a potential strength for reproducibility and extensibility.

major comments (2)
  1. [Abstract] Abstract: the assertion of 'practical relevance' from experiments provides no success rates, benchmark diversity, failure modes, or measures of manual tuning effort required for GPiD theories or Why3 VCs. This directly undermines evaluation of the genericity and laziness claims, as both rest on GPiD routinely emitting precisely the invariants needed without per-program extensions.
  2. [Abstract] The weakest assumption—that abductive reasoning in GPiD will produce invariants sufficient to discharge Why3-generated VCs across a wide range of programs and theories without extensive manual tuning—is stated but not tested or quantified in the provided description. No derivation details, error measures, or data on candidate quality are supplied.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and constructive comments on our manuscript. We address each major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the assertion of 'practical relevance' from experiments provides no success rates, benchmark diversity, failure modes, or measures of manual tuning effort required for GPiD theories or Why3 VCs. This directly undermines evaluation of the genericity and laziness claims, as both rest on GPiD routinely emitting precisely the invariants needed without per-program extensions.

    Authors: We agree the abstract is concise and omits quantitative details. Section 5 of the full manuscript reports experimental results on benchmarks drawn from the Why3 gallery and additional examples, including success rates and the range of theories used. To strengthen the abstract's support for the genericity and laziness claims, we will revise it to briefly reference these outcomes and the absence of per-program theory extensions in the reported cases. revision: yes

  2. Referee: [Abstract] The weakest assumption—that abductive reasoning in GPiD will produce invariants sufficient to discharge Why3-generated VCs across a wide range of programs and theories without extensive manual tuning—is stated but not tested or quantified in the provided description. No derivation details, error measures, or data on candidate quality are supplied.

    Authors: The experiments section evaluates the assumption by applying the method to programs over multiple Why3 theories, showing that GPiD-generated candidates suffice to discharge the VCs in the reported cases. Derivation details and candidate handling appear in Sections 3 and 4. We will revise the abstract to note that the approach was tested across a range of programs and theories without requiring program-specific manual tuning of GPiD. revision: yes

Circularity Check

0 steps flagged

No circularity; relies on independent external tools GPiD and Why3 with no self-referential derivations or fitted predictions

full rationale

The paper presents a system description that integrates two pre-existing external tools (GPiD for abduction and Why3 for verification) to synthesize loop invariants. No equations, parameters, or derivation steps are defined in terms of the target outputs. No self-citations are invoked as load-bearing premises. The genericity and laziness claims are empirical assertions about the external tools' behavior rather than reductions by construction within the paper itself. This is a standard non-circular integration of independent components.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review yields no explicit free parameters, axioms, or invented entities; the approach depends on the correctness and coverage of the external GPiD and Why3 systems.

pith-pipeline@v0.9.0 · 5617 in / 1006 out tokens · 16296 ms · 2026-05-25T15:20:00.935349+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages

  1. [1]

    http://toccata.lri.fr/gallery/

    work page

  2. [2]

    http://pauillac.inria.fr/~levy//why3/sorting/

    work page

  3. [3]

    https://www.lri.fr/~sboldo/research.html

    work page

  4. [4]

    http://pub.ist.ac.at/agupta/invgen/

    Invgen tool. http://pub.ist.ac.at/agupta/invgen/

    work page

  5. [5]

    http://www.nec-labs.com/research/system/systemsSAV-website/benchmarks.php

    Neclabs necla verification benchmarks. http://www.nec-labs.com/research/system/systemsSAV-website/benchmarks.php

    work page

  6. [6]

    https://github.com/sellamiy/GPiD-Framework

    Abdulot framework/GPiD-Ilinva tool suite. https://github.com/sellamiy/GPiD-Framework

    work page

  7. [7]

    Beyer, T

    D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko . Invariant synthesis for combined theories. In Verification, Model Checking, and Abstract Interpreta- tion, 8th International Conference, VMCAI 2007, Nice, Proc eedings, 2007

    work page 2007

  8. [8]

    A. R. Bradley. IC3 and beyond: Incremental, inductive ver ification. In Computer Aided Verification - 24th International Conference, CA V 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings , page 4, 2012

    work page 2012

  9. [9]

    A. R. Bradley and Z. Manna. Property-directed increment al invariant generation. Formal Asp. Comput. , 20(4-5):379–405, 2008

    work page 2008

  10. [10]

    Cousot and N

    P. Cousot and N. Halbwachs. Automatic discovery of linea r restraints among vari- ables of a program. In Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages , POPL ’78, New York, 1978. ACM

    work page 1978

  11. [11]

    E. W. Dijkstra. A Discipline of Programming . Prentice Hall PTR, Upper Saddle River, NJ, USA, 1st edition, 1997

    work page 1997

  12. [12]

    Dillig, T

    I. Dillig, T. Dillig, B. Li, and K. L. McMillan. Inductive invariant generation via abductive inference. In A. L. Hosking, P. T. Eugster, and C. V . Lopes, editors, Proceedings of OOPSLA 2013, Indianapolis , pages 443–456. ACM, 2013

    work page 2013

  13. [13]

    Echenim, N

    M. Echenim, N. Peltier, and Y. Sellami. A generic framewo rk for implicate gen- eration modulo theories. In D. Galmiche, S. Schulz, and R. Se bastiani, editors, IJCAR 2018, Oxford , volume 10900 of LNCS, pages 279–294. Springer, 2018

    work page 2018

  14. [14]

    M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dy namically discovering likely program invariants to support program evolution. In Proceedings of the 21st International Conference on Software Engineering , ICSE ’99, pages 213–224, New York, NY, USA, 1999. ACM

    work page 1999

  15. [15]

    Filliˆ atre and A

    J.-C. Filliˆ atre and A. Paskevich. Why3 — where programs meet provers. In M. Felleisen and P. Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science , pages 125–

    work page

  16. [16]

    Flanagan and K

    C. Flanagan and K. R. M. Leino. Houdini, an annotation ass istant for esc/java. In J. N. Oliveira and P. Zave, editors, FME 2001: Formal Methods for Increasing Software Productivity , pages 500–517, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg

    work page 2001

  17. [17]

    Ghilardi and S

    S. Ghilardi and S. Ranise. Backward reachability of arra y-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Sci- ence, 6(4), 2010

    work page 2010

  18. [18]

    T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Soft ware verification with blast. In T. Ball and S. K. Rajamani, editors, Model Checking Software , pages 235–239, Berlin, Heidelberg, 2003. Springer Berlin Heidel berg

    work page 2003

  19. [19]

    C. A. R. Hoare. An axiomatic basis for computer programmi ng. Commun. ACM , 12(10):576–580, Oct. 1969

    work page 1969

  20. [20]

    D. Kapur. A quantifier-elimination based heuristic for a utomatically generating inductive assertions for programs. J. Systems Science & Complexity , 19, 2006

    work page 2006

  21. [21]

    Karbyshev, N

    A. Karbyshev, N. Bjørner, S. Itzhaky, N. Rinetzky, and S. Shoham. Property- directed inference of universal invariants or proving thei r absence. J. ACM , 64(1):7:1–7:33, 2017

    work page 2017

  22. [22]

    Kov´ acs and A

    L. Kov´ acs and A. Voronkov. Finding loop invariants for p rograms over arrays using a theorem prover. In Fundamental Approaches to Software Engineering, 12th International Conference, F ASE 2009, Held as Part of th e Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, pages 470–485, 2009

    work page 2009

  23. [23]

    Kov´ acs and A

    L. Kov´ acs and A. Voronkov. Interpolation and symbol eli mination. In Automated Deduction - CADE-22, 22nd International Conference on Auto mated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings , pages 199–213, 2009

    work page 2009

  24. [24]

    A. Min´ e. The octagon abstract domain. Higher Order Symbol. Comput. , 19, 2006

    work page 2006

  25. [25]

    Padon, N

    O. Padon, N. Immerman, S. Shoham, A. Karbyshev, and M. Sag iv. Decidability of inferring inductive invariants. In Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, P OPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 , pages 217–231, 2016

    work page 2016

  26. [26]

    Suzuki and K

    N. Suzuki and K. Ishihata. Implementation of an array bou nd checker. 1977

    work page 1977