Interval polyhedra: An abstract domain to infer interval linear relationships

Abstract

We introduce a new numerical abstract domain, so-called interval polyhedra (itvPol), to infer and propagate interval linear constraints over program variables. itvPol, which allows to represent constraints of the form Σk[ak, bk]xk ≤ c, is more expressive than the classic convex polyhedra domain and allows to express certain non-convex (even unconnected) properties. The implementation of itvPol can be constructed based on interval linear programming and an interval variant of Fourier-Motzkin elimination. The preliminary experimental results of our prototype are encouraging, especially for programs affected by interval uncertainty, e.g., due to uncertain input data or interval-based abstractions of disjunctive, non-linear, or floating-point expressions. To our knowledge, this is the first application of interval linear algebra to static analysis. © 2009 Springer.