Interval polyhedra: An abstract domain to infer interval linear relationships

Liqian Chen, Antoine Miné, Ji Wang, Patrick Cousot

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 16th International Symposium, SAS 2009, Proceedings
Number of pages17
StatePublished - 2009
Event16th International Symposium on Static Analysis, SAS 2009 - Los Angeles, CA, United States
Duration: Aug 9 2009Aug 11 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5673 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other16th International Symposium on Static Analysis, SAS 2009
Country/TerritoryUnited States
CityLos Angeles, CA

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Interval polyhedra: An abstract domain to infer interval linear relationships'. Together they form a unique fingerprint.

Cite this