Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships

Polyhedra: An Abstract Domain to Infer Interval Linear Relationships Liqian Chen1,2 , Antoine Min?e2,3 , Ji Wang1 , and Patrick Cousot2,4 1 National Laboratory for Parallel and Distributed Processing, Changsha, P.R.China [e-mail] 2 ?Ecole Normale Sup?erieure, Paris, France {chen,mine,cousot}@di.ens.fr 3 CNRS, France 4 CIMS, New York University, New York, NY, USA 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 uncerta...

• Type: Conference
• Year: 2009
• Where: SAS
• Authors: Antoine Miné, Ji Wang, Liqian Chen, Patrick Cousot
• Keywords: Formal Methods, Interval Linear Algebra, Interval Linear Constraints, SAS 2009, So-called Interval Polyhedra