An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs
Antoine Miné, Jason Breck, and Thomas Reps
This paper addresses the problem of proving a given
invariance property φ of a loop in a numeric program,
by inferring automatically a stronger inductive invariant ψ.
The algorithm we present is based on both abstract
interpretation and constraint solving.
As in abstract interpretation, it computes the effect of a loop using
a numeric abstract domain.
As in constraint satisfaction, it works from ``above''—interactively
splitting and tightening a collection of abstract elements until an
inductive invariant is found.
Our experiments show that the algorithm can find non-linear inductive
invariants that cannot normally be obtained using intervals (or octagons),
even when classic techniques for increasing abstract-interpretation
precision are employed—such as increasing and decreasing iterations
with extrapolation, partitioning, and disjunctive completion.
The advantage of our work is that because the algorithm uses standard
abstract domains, it sidesteps the need to develop complex,
non-standard domains specialized for solving a particular problem.
(Click here to access the paper:
PDF.)