Interval polyhedra: An abstract domain to infer interval linear relationships

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

doi:10.1007/978-3-642-03237-0_21

Interval polyhedra: An abstract domain to infer interval linear relationships

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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[a_k, b_k]x_k ≤ 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 language	English (US)
Title of host publication	Static Analysis - 16th International Symposium, SAS 2009, Proceedings
Pages	309-325
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-642-03237-0_21
State	Published - 2009
Event	16th International Symposium on Static Analysis, SAS 2009 - Los Angeles, CA, United States Duration: Aug 9 2009 → Aug 11 2009

Publication series

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

Other

Other	16th International Symposium on Static Analysis, SAS 2009
Country/Territory	United States
City	Los Angeles, CA
Period	8/9/09 → 8/11/09

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

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

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

Interval polyhedra: An abstract domain to infer interval linear relationships. / Chen, Liqian; Miné, Antoine; Wang, Ji et al.
Static Analysis - 16th International Symposium, SAS 2009, Proceedings. 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 proceeding › Conference 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. 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. 2009. p. 309-325. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-03237-0_21

@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",

note = "Funding Information: This work is supported by the INRIA project “Abstraction” common to CNRS and ENS in France, and by the National Natural Science Foundation of China under Grant No.60725206.; 16th International Symposium on Static Analysis, SAS 2009 ; Conference date: 09-08-2009 Through 11-08-2009",

year = "2009",

doi = "10.1007/978-3-642-03237-0_21",

language = "English (US)",

isbn = "3642032362",

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 - 16th International Symposium on Static Analysis, SAS 2009

AU - Chen, Liqian

AU - Miné, Antoine

AU - Wang, Ji

AU - Cousot, Patrick

N1 - Funding Information: This work is supported by the INRIA project “Abstraction” common to CNRS and ENS in France, and by the National Natural Science Foundation of China under Grant No.60725206.

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

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

Y2 - 9 August 2009 through 11 August 2009

ER -

Interval polyhedra: An abstract domain to infer interval linear relationships

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this