School of Computing

The Two Variable Per Inequality Abstract Domain

Axel Simon, Andy King, and Jacob M. Howe

Higher-Order and Symbolic Computation, 31(1):182-196, March 2010 Note the Springer published the *wrong* version of this paper in HOSC and this on-line version of the paper should be taken as final.

Abstract

This article presents the Two Variable Per Inequality abstract domain (TVPI domain for short). This so-called weakly-relational domain is able to express systems of linear inequalities where each inequality has at most two variables. The domain represents a sweet-point in the performance-cost tradeoff between the faster Octagon domain and the more expressive domain of general convex polyhedra. In particular, we detail techniques to closely approximate integral TVPI systems, thereby finessing the problem of excessively growing coefficients, yielding -- to our knowledge -- the only relational domain that combines linear relations with arbitrary coefficients and strongly polynomial performance.

Download publication 1131 kbytes (PDF)

Bibtex Record

@article{3167,
author = {Axel Simon and Andy King and Jacob M. Howe},
title = {The {T}wo {V}ariable {P}er {I}nequality {A}bstract {D}omain},
month = {March},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Note the Springer published the *wrong* version of this paper in HOSC and this on-line version of the paper should be taken as final.},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2010/3167},
    publication_type = {article},
    submission_id = {26216_1316789595},
    journal = {Higher-Order and Symbolic Computation},
    volume = {31},
    number = {1},
    publisher = {Springer},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014