Interpolating Quantifier-Free Presburger Arithmetic
Interpolating Quantifier-Free Presburger Arithmetic
复制标题
内插无量词 Presburger 算法
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Philipp Rümmer
中科院分区：
文献类型：
--
作者：
D. Kroening;Jérôme Leroux;Philipp Rümmer
Craig插值已成为许多符号模型检查器中的关键要素，可作为昂贵的量化器消除的近似替代品。在本文中，我们关注的是，用于整体算术算术的完整无量化片段的插值决策程序，即整数上的线性算术，这是一种非常适合软件系统分析的理论。与基于量化器消除和欧米茄测试的早期程序相反，我们的方法使用整数线性编程技术：对理性的插值问题放松，以及针对有效插值量身定制的完整分支和结合规则。方程是通过专用的多项式子处理来处理的。我们已经在SMT-Solver OpenSMT之上完全实施了我们的程序，并进行了广泛的实验评估。
Craig interpolation has become a key ingredient in many symbolic model checkers, serving as an approximative replacement for expensive quantifier elimination. In this paper, we focus on an interpolating decision procedure for the full quantifier-free fragment of Presburger Arithmetic, i.e., linear arithmetic over the integers, a theory which is a good fit for the analysis of software systems. In contrast to earlier procedures based on quantifier elimination and the Omega test, our approach uses integer linear programming techniques: relaxation of interpolation problems to the rationals, and a complete branch-and-bound rule tailored to efficient interpolation. Equations are handled via a dedicated polynomial-time sub-procedure. We have fully implemented our procedure on top of the SMT-solver OpenSMT and present an extensive experimental evaluation.