School of Computing

Widening Polyhedra with Landmarks

Axel Simon and Andy King

In Naoki Kobayashi, editor, Fourth Asian Symposium on Programming Languages and Systems, volume 4279 of Lecture Notes in Computer Science, pages 182-196. Springer Verlag, November 2006 See also


The abstract domain of polyhedra is sufficiently expressive to be deployed in verification. One consequence of the richness of this domain is that long, possibly infinite, sequences of polyhedra can arise in the analysis of loops. Widening and narrowing have been proposed to infer a single polyhedron that summarises such a sequence of polyhedra. Motivated by precision losses encountered in verification, we explain how the classic widening/narrowing approach can be refined by an improved extrapolation strategy. The insight is to record inequalities that are thus far found to be unsatisfiable in the analysis of a loop. These so-called landmarks hint at the amount of widening necessary to reach stability. This extrapolation strategy, which refines widening with thresholds, can infer post-fixpoints that are precise enough not to require narrowing. Unlike previous techniques, our approach interacts well with other domains, is fully automatic, conceptually simple and precise on complex loops.

Download publication 325 kbytes (PDF)

Bibtex Record

author = {Axel Simon and Andy King},
title = {{W}idening {P}olyhedra with {L}andmarks},
month = {November},
year = {2006},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {See also},
doi = {},
url = {},
    publication_type = {inproceedings},
    submission_id = {4886_1154700407},
    booktitle = {Fourth Asian Symposium on Programming Languages and Systems},
    editor = {Naoki Kobayashi},
    series = {Lecture Notes in Computer Science},
    publisher = {Springer Verlag},
    refereed = {yes},
    volume = {4279},
    ISBN = {3-540-48937-1},

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

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

Last Updated: 21/03/2014