A sound floating-point polyhedra abstract domain

Liqian Chen, Antoine Miné, Patrick Cousot

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

Abstract

The polyhedra abstract domain is one of the most powerful and commonly used numerical abstract domains in the field of static program analysis based on abstract interpretation. In this paper, we present an implementation of the polyhedra domain using floating-point arithmetic without sacrificing soundness. Floating-point arithmetic allows a compact memory representation and an efficient implementation on current hardware, at the cost of some loss of precision due to rounding. Our domain is based on a constraint-only representation and employs sound floating-point variants of Fourier-Motzkin elimination and linear programming. The preliminary experimental results of our prototype are encouraging. To our knowledge, this is the first time that the polyhedra domain is adapted to floating-point arithmetic in a sound way.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings
Pages3-18
Number of pages16
Volume5356 LNCS
DOIs
StatePublished - 2008
Event6th Asian Symposium on Programming Languages and Systems, APLAS 2008 - Bangalore, India
Duration: Dec 9 2008Dec 11 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5356 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other6th Asian Symposium on Programming Languages and Systems, APLAS 2008
CountryIndia
CityBangalore
Period12/9/0812/11/08

Fingerprint

Digital arithmetic
Floating point
Polyhedron
Floating-point Arithmetic
Acoustic waves
Linear programming
Computer hardware
Abstract Interpretation
Program Analysis
Rounding
Data storage equipment
Static Analysis
Soundness
Efficient Implementation
Elimination
Sound
Hardware
Prototype
Experimental Results

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Chen, L., Miné, A., & Cousot, P. (2008). A sound floating-point polyhedra abstract domain. In Programming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings (Vol. 5356 LNCS, pp. 3-18). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5356 LNCS). https://doi.org/10.1007/978-3-540-89330-1-2

A sound floating-point polyhedra abstract domain. / Chen, Liqian; Miné, Antoine; Cousot, Patrick.

Programming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings. Vol. 5356 LNCS 2008. p. 3-18 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5356 LNCS).

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

Chen, L, Miné, A & Cousot, P 2008, A sound floating-point polyhedra abstract domain. in Programming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings. vol. 5356 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5356 LNCS, pp. 3-18, 6th Asian Symposium on Programming Languages and Systems, APLAS 2008, Bangalore, India, 12/9/08. https://doi.org/10.1007/978-3-540-89330-1-2
Chen L, Miné A, Cousot P. A sound floating-point polyhedra abstract domain. In Programming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings. Vol. 5356 LNCS. 2008. p. 3-18. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-89330-1-2
Chen, Liqian ; Miné, Antoine ; Cousot, Patrick. / A sound floating-point polyhedra abstract domain. Programming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings. Vol. 5356 LNCS 2008. pp. 3-18 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{d0ab97d8d8cd4f49bc5da77085533e9e,
title = "A sound floating-point polyhedra abstract domain",
abstract = "The polyhedra abstract domain is one of the most powerful and commonly used numerical abstract domains in the field of static program analysis based on abstract interpretation. In this paper, we present an implementation of the polyhedra domain using floating-point arithmetic without sacrificing soundness. Floating-point arithmetic allows a compact memory representation and an efficient implementation on current hardware, at the cost of some loss of precision due to rounding. Our domain is based on a constraint-only representation and employs sound floating-point variants of Fourier-Motzkin elimination and linear programming. The preliminary experimental results of our prototype are encouraging. To our knowledge, this is the first time that the polyhedra domain is adapted to floating-point arithmetic in a sound way.",
author = "Liqian Chen and Antoine Min{\'e} and Patrick Cousot",
year = "2008",
doi = "10.1007/978-3-540-89330-1-2",
language = "English (US)",
isbn = "3540893296",
volume = "5356 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "3--18",
booktitle = "Programming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings",

}

TY - GEN

T1 - A sound floating-point polyhedra abstract domain

AU - Chen, Liqian

AU - Miné, Antoine

AU - Cousot, Patrick

PY - 2008

Y1 - 2008

N2 - The polyhedra abstract domain is one of the most powerful and commonly used numerical abstract domains in the field of static program analysis based on abstract interpretation. In this paper, we present an implementation of the polyhedra domain using floating-point arithmetic without sacrificing soundness. Floating-point arithmetic allows a compact memory representation and an efficient implementation on current hardware, at the cost of some loss of precision due to rounding. Our domain is based on a constraint-only representation and employs sound floating-point variants of Fourier-Motzkin elimination and linear programming. The preliminary experimental results of our prototype are encouraging. To our knowledge, this is the first time that the polyhedra domain is adapted to floating-point arithmetic in a sound way.

AB - The polyhedra abstract domain is one of the most powerful and commonly used numerical abstract domains in the field of static program analysis based on abstract interpretation. In this paper, we present an implementation of the polyhedra domain using floating-point arithmetic without sacrificing soundness. Floating-point arithmetic allows a compact memory representation and an efficient implementation on current hardware, at the cost of some loss of precision due to rounding. Our domain is based on a constraint-only representation and employs sound floating-point variants of Fourier-Motzkin elimination and linear programming. The preliminary experimental results of our prototype are encouraging. To our knowledge, this is the first time that the polyhedra domain is adapted to floating-point arithmetic in a sound way.

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

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

U2 - 10.1007/978-3-540-89330-1-2

DO - 10.1007/978-3-540-89330-1-2

M3 - Conference contribution

SN - 3540893296

SN - 9783540893295

VL - 5356 LNCS

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

SP - 3

EP - 18

BT - Programming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings

ER -