A CLP Method for Compositional and Intermittent Predicate Abstraction
A CLP Method for Compositional and Intermittent Predicate Abstraction
复制标题
组合谓词和断续谓词抽象的CLP方法
DOI：
10.1007/11609773_2
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
R. Voicu
中科院分区：
文献类型：
--
作者：
J. Jaffar;A. Santosa;R. Voicu
我们提出了一个符号可达性分析的实现，具有组合性和间歇性抽象的特征，在只在选定的程序点执行近似的意义上，如果有的话。组合性的主要优点是众所周知的，而间歇抽象的优点是确保算法收敛所需的抽象域可以最小化，并且执行抽象的成本（现在是间歇的）降低了。我们从在CLP中表述问题开始，并首先获得组合性。然后，我们解决了两个关键的效率挑战。首先，需要对与任意长程序片段相关联的最强后置条件操作符进行推理。这本质上意味着要处理无数变量的约束，这些变量描述了手头程序片段的开始和结束之间的状态。这可以通过使用CLP系统中隐含的变量消除或投影机制来解决。第二个挑战是终止，即确定哪些子目标是冗余的。我们通过一种新的称为共归纳表的记忆公式来解决这个问题。最后对该方法进行了实验验证。在一种极端情况下，每个步骤都执行抽象，我们与模型检查器进行比较。在另一种极端情况下，没有执行抽象，我们与程序验证器进行比较。当然，我们的方法提供了一个中间地带，灵活地结合了抽象和hoare风格的推理以及谓词转换和循环不变量。
We present an implementation of symbolic reachability analysis with the features of compositionality, andintermittentabstraction, in the sense of pefrorming approximation only at selected program points, if at all. The key advantages of compositionality are well known, while those of intermittent abstraction are that the abstract domain required to ensure convergence of the algorithm can be minimized, and that the cost of performing abstractions, now being intermittent, is reduced.We start by formulating the problem in CLP, and first obtain compositionality. We then address two key efficiency challenges. The first is that reasoning is required about the strongest-postcondition operator associated with an arbitrarily long program fragment. This essentially means dealing with constraints over an unbounded number of variables describing the states between the start and end of the program fragment at hand. This is addressed by using the variable elimination or projection mechanism that is implicit in CLP systems. The second challenge is termination, that is, to determine which subgoals are redundant. We address this by a novel formulation of memoization calledcoinductive tabling.We finally evaluate the method experimentally. At one extreme, where abstraction is performed at every step, we compare against a model checker. At the other extreme, where no abstraction is performed, we compare against a program verifier. Of course, our method provides for the middle ground, with a flexible combination of abstraction and Hoare-style reasoning with predicate transformers and loop-invariants.