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

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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 16th International Symposium, SAS 2009, Proceedings
Pages309-325
Number of pages17
DOIs
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

Other

Other16th International Symposium on Static Analysis, SAS 2009
CountryUnited States
CityLos Angeles, CA
Period8/9/098/11/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Chen, L., Miné, A., Wang, J., & Cousot, P. (2009). Interval polyhedra: An abstract domain to infer interval linear relationships. In Static Analysis - 16th International Symposium, SAS 2009, Proceedings (pp. 309-325). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5673 LNCS). https://doi.org/10.1007/978-3-642-03237-0_21