Playing in the grey area of proofs
Playing in the grey area of proofs
复制标题
DOI：
10.1145/2103656.2103689
复制
发表时间：
2012-01
期刊：
影响因子：
--
通讯作者：
Krystof Hoder;L. Kovács;A. Voronkov
中科院分区：
文献类型：
--
作者：
Krystof Hoder;L. Kovács;A. Voronkov
插值是程序验证和静态分析中的一项重要技术。特别是，从各种属性的证明中提取的插值用于不变量生成和有界模型检查。最近的一些论文研究插值在各种理论和提取较小的插值证明。特别是，有几种算法用于从所谓的局部证明中提取插值。本文的主要贡献是一种技术，最小化插值变换的基础上，我们称之为“灰色区域”的本地证明。另一个贡献是一种技术的转换，在某些共同的条件下，任意证明到当地的。不像许多其他插值技术，我们的技术是非常普遍的，适用于任意的理论。我们的方法是实现在定理证明吸血鬼和大量的基准来自一阶定理证明和有界模型检查使用逻辑与平等，未解释的功能和线性整数运算进行评估。我们的实验证明了新技术的力量：例如，这是不寻常的，我们的证明变换提供了超过十倍的插值大小减少。
Interpolation is an important technique in verification and static analysis of programs. In particular, interpolants extracted from proofs of various properties are used in invariant generation and bounded model checking. A number of recent papers studies interpolation in various theories and also extraction of smaller interpolants from proofs. In particular, there are several algorithms for extracting of interpolants from so-called local proofs. The main contribution of this paper is a technique of minimising interpolants based on transformations of what we call the "grey area" of local proofs. Another contribution is a technique of transforming, under certain common conditions, arbitrary proofs into local ones. Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear integer arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants.