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
Volume5673 LNCS
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Linear algebra
Static analysis
Polyhedron
Linear programming
Interval
Uncertainty
Relationships
Convex polyhedron
Floating point
Static Analysis
Linear Constraints
Elimination
Express
Prototype
Experimental Results

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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 (Vol. 5673 LNCS, 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

Interval polyhedra : An abstract domain to infer interval linear relationships. / Chen, Liqian; Miné, Antoine; Wang, Ji; Cousot, Patrick.

Static Analysis - 16th International Symposium, SAS 2009, Proceedings. Vol. 5673 LNCS 2009. p. 309-325 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5673 LNCS).

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

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. vol. 5673 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5673 LNCS, pp. 309-325, 16th International Symposium on Static Analysis, SAS 2009, Los Angeles, CA, United States, 8/9/09. https://doi.org/10.1007/978-3-642-03237-0_21
Chen L, Miné A, Wang J, Cousot P. Interval polyhedra: An abstract domain to infer interval linear relationships. In Static Analysis - 16th International Symposium, SAS 2009, Proceedings. Vol. 5673 LNCS. 2009. p. 309-325. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-03237-0_21
Chen, Liqian ; Miné, Antoine ; Wang, Ji ; Cousot, Patrick. / Interval polyhedra : An abstract domain to infer interval linear relationships. Static Analysis - 16th International Symposium, SAS 2009, Proceedings. Vol. 5673 LNCS 2009. pp. 309-325 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{94dabdb8637a43cd975050ff628c8228,
title = "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.",
author = "Liqian Chen and Antoine Min{\'e} and Ji Wang and Patrick Cousot",
year = "2009",
doi = "10.1007/978-3-642-03237-0_21",
language = "English (US)",
isbn = "3642032362",
volume = "5673 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "309--325",
booktitle = "Static Analysis - 16th International Symposium, SAS 2009, Proceedings",

}

TY - GEN

T1 - Interval polyhedra

T2 - An abstract domain to infer interval linear relationships

AU - Chen, Liqian

AU - Miné, Antoine

AU - Wang, Ji

AU - Cousot, Patrick

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=70350302846&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70350302846&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-03237-0_21

DO - 10.1007/978-3-642-03237-0_21

M3 - Conference contribution

AN - SCOPUS:70350302846

SN - 3642032362

SN - 9783642032363

VL - 5673 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 309

EP - 325

BT - Static Analysis - 16th International Symposium, SAS 2009, Proceedings

ER -