Skip to main content

Widening Polyhedra with Landmarks: 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006. Proceedings

Simon, Axel and King, Andy (2007) Widening Polyhedra with Landmarks: 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006. Proceedings. In: Kobayashi, Naoki, ed. Asian Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, 4279 . Springer, pp. 166-182. ISBN 978-3-540-48937-5. (doi:10.1007/11924661_11) (KAR id:37597)

Abstract

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.

Item Type: Book section
DOI/Identification number: 10.1007/11924661_11
Subjects: A General Works
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 12 Dec 2013 22:39 UTC
Last Modified: 16 Nov 2021 10:14 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/37597 (The current URI for this page, for reference purposes)

University of Kent Author Information

Simon, Axel.

Creator's ORCID:
CReDIT Contributor Roles:

King, Andy.

Creator's ORCID: https://orcid.org/0000-0001-5806-4822
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.