MINDS @ UW-Madison

An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs

Show full item record


Mine, Antoine; Breck, Jason; Reps, Thomas
Jan 08, 2016
numeric properties; inductive invariant; constraint solving; abstract interpretation; invariant
This paper addresses the problem of proving a given invariance property phi of a loop in a numeric program, by inferring automatically a stronger inductive invariant psi. 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.
Permanent link
Export to RefWorks 

Part of

Show full item record

Search and browse


Deposit materials

  1. Register to deposit in MINDS@UW
  2. Need deposit privileges? Contact us.
  3. Already registered? Have deposit privileges? Deposit materials.