An abstract domain to discover interval linear equalities

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

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


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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings
Number of pages17
StatePublished - 2010
Event11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010 - Madrid, Spain
Duration: Jan 17 2010Jan 19 2010

Publication series

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


Other11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'An abstract domain to discover interval linear equalities'. Together they form a unique fingerprint.

Cite this