Widening Polyhedra with Landmarks
Widening Polyhedra with Landmarks
复制标题
带地标的加宽多面体
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
A. King
中科院分区：
文献类型：
--
作者：
A. Simon;A. King
Polyhedra的抽象领域足够表达，可以在验证中部署。该领域丰富性的结果之一是，在回路的分析中，可能会出现漫长的，可能是无限的多层次序列。已经提出扩大和狭窄来推断一个多面体，总结了这样的多面体。在验证中遇到的精确损失的动机中，我们解释了如何通过改进的外推策略来完善经典的扩大/狭窄方法。洞察力是记录迄今为止在循环分析中不满意的不平等现象。这些所谓的地标暗示了达到稳定所需的扩大量。这种推断策略可以通过阈值来完善扩大，可以推断出固定的后点，这些后点足够精确，不需要缩小。与以前的技术不同，我们的方法与其他域相互作用，在复杂循环中是完全自动的，在概念上是简单而精确的。
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.