School of Computing

Logahedra: a New Weakly Relational Domain

Jacob M. Howe and Andy King

In Zhiming Lu and Anders P. Ravn, editors, International Symposium on Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, October 2009.

Abstract

Weakly relational numeric domains express restricted classes of linear inequalities that strike a balance between what can be described and what can be efficiently computed. Popular weakly relational domains such as bounded differences and octagons have found application in model checking and abstract interpretation. This paper introduces logahedra, which are more expressiveness than octagons, but less expressive than arbitrary systems of two variable per inequality constraints. Logahedra allow coefficients of inequalities to be powers of two whilst retaining many of the desirable algorithmic properties of octagons.

Download publication 238 kbytes (PDF)

Bibtex Record

@inproceedings{2926,
author = {Jacob M. Howe and Andy King},
title = {Logahedra: a {N}ew {W}eakly {R}elational {D}omain},
month = {October},
year = {2009},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2009/2926},
    publication_type = {inproceedings},
    submission_id = {24909_1245169132},
    booktitle = {International Symposium on Automated Technology for Verification and Analysis},
    editor = {Zhiming Lu and Anders P. Ravn},
    series = {Lecture Notes in Computer Science},
    publisher = {Springer-Verlag},
    refereed = {yes},
}

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

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

Last Updated: 21/03/2014