Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
Liqian Chen, Antoine Miné, Ji Wang, Patrick M. Cousot · 2009
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. 1