×

zbMATH — the first resource for mathematics

An abstract domain to discover interval linear equalities. (English) Zbl 1273.68081
Barthe, Gilles (ed.) et al., Verification, model checking, and abstract interpretation. 11th international conference, VMCAI 2010, Madrid, Spain, January 17–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11318-5/pbk). Lecture Notes in Computer Science 5944, 112-128 (2010).
Summary: 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.
For the entire collection see [Zbl 1178.68003].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
65F99 Numerical linear algebra
65G40 General methods in interval analysis
Software:
Apron; Octagon
PDF BibTeX XML Cite
Full Text: DOI