© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Two Variables per Linear Inequality as an Abstract Domain
Axel Simon, Andy King, and Jacob M. Howe
In M. Leuschel, editor, Proceedings of Logic Based Program Development and Transformation, volume 2664 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, 2002 see http://www.springer.de./comp/lncs/index.html.Abstract
This paper explores the spatial domain of sets of inequalities where each inequality contains at most two variables - a domain that is richer than intervals and more tractable than general polyhedra. We present a complete suite of efficient domain operations for linear systems with two variables per inequality with unrestricted coefficients. We exploit a tactic in which a system of inequalities with at most two variables per inequality is decomposed into a series of projections - one for each two dimensional plane. The decomposition enables all domain operations required for abstract interpretation to be expressed in terms of the two dimensional case. The resulting operations are efficient and include a novel planar convex hull algorithm. Empirical evidence suggests that widening can be applied effectively, ensuring tractability.
Download publication
407 kbytes
(PostScript)
Bibtex Record
@inproceedings{1515,
author = {Axel Simon and Andy King and Jacob M. Howe},
title = {Two {V}ariables per {L}inear {I}nequality as an {A}bstract {D}omain},
month = {unknown},
year = {2002},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {see http://www.springer.de./comp/lncs/index.html},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2002/1515},
publication_type = {inproceedings},
submission_id = {13588_1033461366},
refereed = {yes},
series = {Lecture Notes in Computer Science},
booktitle = {Proceedings of Logic Based Program Development and Transformation},
publisher = {Springer-Verlag},
volume = {2664},
editor = {M. Leuschel},
}