Sciweavers

Share
ESOP
2016
Springer

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

4 years 3 months ago
An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs
Abstract. 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 domain. As in constraint satisfaction, it works from “above”— ively 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, no...
Antoine Miné, Jason Breck, Thomas W. Reps
Added 03 Apr 2016
Updated 03 Apr 2016
Type Journal
Year 2016
Where ESOP
Authors Antoine Miné, Jason Breck, Thomas W. Reps
Comments (0)
books