Complete Instantiation-Based Interpolation
Complete Instantiation-Based Interpolation
复制标题
完整的基于实例化的插值
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Thomas Wies
中科院分区：
文献类型：
--
作者：
Nishant Totla;Thomas Wies
克雷格插值一直是程序分析和验证中的一个有价值的工具。现代 SMT 求解器为这些应用中最常用的理论实现插值过程。然而，许多特定于应用的理论仍然不受支持，这限制了基于插值的技术适用的问题类别。在本文中，我们提出了一个通用框架，通过减少现有的插值过程来构建新的插值过程。我们考虑这样的情况：特定于应用的理论可以形式化为具有附加符号和公理的基础理论的扩展。我们的技术使用扩展公理的有限实例化来将理论扩展中的插值问题减少到基础理论中的插值问题。我们确定了一个模型理论标准，使我们能够检测我们的技术是否完整的情况。我们讨论与程序验证相关且满足该标准的具体理论。特别是，我们获得了数组和链表理论的完整插值过程。后者是支持对堆分配数据结构的复杂形状属性进行推理的理论的第一个完整插值过程。
Craig interpolation has been a valuable tool in program analysis and verification. Modern SMT solvers implement interpolation procedures for the theories that are most commonly used in these applications. However, many application-specific theories remain unsupported, which limits the class of problems to which interpolation-based techniques apply. In this paper, we present a generic framework to build new interpolation procedures via a reduction to existing interpolation procedures. We consider the case where an application-specific theory can be formalized as an extension of a base theory with additional symbols and axioms. Our technique uses finite instantiation of the extension axioms to reduce an interpolation problem in the theory extension to one in the base theory. We identify a model-theoretic criterion that allows us to detect the cases where our technique is complete. We discuss specific theories that are relevant in program verification and that satisfy this criterion. In particular, we obtain complete interpolation procedures for theories of arrays and linked lists. The latter is the first complete interpolation procedure for a theory that supports reasoning about complex shape properties of heap-allocated data structures.
反例引导焦点
DOI：
10.1145/1706299.1706330
发表时间：
2010
期刊：
影响因子：
--
作者：
A. Podelski;T. Wies
通讯作者：
T. Wies