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)
Download (341kB)
Preview
|
|
|
Official URL http://dx.doi.org/10.1007/11924661_11 |
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: | Faculties > Sciences > School of Computing > Programming Languages and Systems Group |
Depositing User: | Andy King |
Date Deposited: | 12 Dec 2013 22:39 UTC |
Last Modified: | 29 May 2019 11:40 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/37597 (The current URI for this page, for reference purposes) |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):