TY - GEN
T1 - An abstract domain to discover interval linear equalities
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 - 2010
Y1 - 2010
N2 - We introduce a new abstract domain, namely the domain of Interval Linear Equalities (itvLinEqs), which generalizes the affine equality domain with interval coefficients by leveraging results from interval linear algebra. The representation of itvLinEqs is based on a row echelon system of interval linear equalities, which natively allows expressing classical linear relations as well as certain topologically non-convex (even unconnected or non-closed) properties. The row echelon form limits the expressiveness of the domain but yields polynomial-time domain operations. Interval coefficients enable a sound adaptation of itvLinEqs to floating-point arithmetic. itvLinEqs can be used to infer and propagate interval linear constraints, especially for programs involving uncertain or inexact data. The preliminary experimental results are encouraging: itvLinEqs can find a larger range of invariants than the affine equality domain. Moreover, itvLinEqs provides an efficient alternative to polyhedra-like domains.
AB - We introduce a new abstract domain, namely the domain of Interval Linear Equalities (itvLinEqs), which generalizes the affine equality domain with interval coefficients by leveraging results from interval linear algebra. The representation of itvLinEqs is based on a row echelon system of interval linear equalities, which natively allows expressing classical linear relations as well as certain topologically non-convex (even unconnected or non-closed) properties. The row echelon form limits the expressiveness of the domain but yields polynomial-time domain operations. Interval coefficients enable a sound adaptation of itvLinEqs to floating-point arithmetic. itvLinEqs can be used to infer and propagate interval linear constraints, especially for programs involving uncertain or inexact data. The preliminary experimental results are encouraging: itvLinEqs can find a larger range of invariants than the affine equality domain. Moreover, itvLinEqs provides an efficient alternative to polyhedra-like domains.
UR - http://www.scopus.com/inward/record.url?scp=77949420260&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77949420260&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-11319-2_11
DO - 10.1007/978-3-642-11319-2_11
M3 - Conference contribution
AN - SCOPUS:77949420260
SN - 3642113184
SN - 9783642113185
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 112
EP - 128
BT - Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings
T2 - 11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010
Y2 - 17 January 2010 through 19 January 2010
ER -