TY - GEN
T1 - A sound floating-point polyhedra abstract domain
AU - Chen, Liqian
AU - Miné, Antoine
AU - Cousot, Patrick
N1 - Funding Information:
This work is supported by the INRIA project-team Abstraction common to the CNRS and the École Normale Supérieure. This work is partially supported by the Fund of the China Scholarship Council and National Natural Science Foundation of China under Grant No.60725206.
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
AN - SCOPUS:58549098897
SN - 3540893296
SN - 9783540893295
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
PB - Springer Verlag
T2 - 6th Asian Symposium on Programming Languages and Systems, APLAS 2008
Y2 - 9 December 2008 through 11 December 2008
ER -