Widening polyhedra with landmarks.

*(English)*Zbl 1168.68365
Kobayashi, Naoki (ed.), Programming languages and systems. 4th Asian symposium, APLAS 2006, Sydney, Australia, November 8–10, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-48937-5/pbk). Lecture Notes in Computer Science 4279, 166-182 (2006).

Summary: 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.

For the entire collection see [Zbl 1133.68007].

For the entire collection see [Zbl 1133.68007].