An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
复制标题
无量词 Presburger 算术的插值顺序微积分
DOI：
10.1007/s10817-011-9237-y
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
T. Wahl
中科院分区：
文献类型：
--
作者：
Angelo Brillout;D. Kroening;Philipp Rümmer;T. Wahl
Craig插值已成为正式验证的多功能工具，例如，用于生成作为循环不变式候选者的程序主张。在本文中，我们考虑了无量词的前爆发算术（QFPA）的Craig插值。直到最近，消除量词是该理论的唯一可用的插值方法，但是，众所周知，这是潜在的代价高昂和僵化的。我们基于QFPA的序列演算引入了一种插值方法，该方法通过注释部分插入剂的不满可证明的步骤来确定插值。我们证明我们的演算是声音和完整的。我们已经扩展了公主定理供奉献者来生成插值证明，并将其应用于大量公开可用的前汉堡算术基准。结果记录了我们的插值程序的鲁棒性和效率。最后，我们将程序与用于QFPA和线性有理算术的替代性插值方法进行了比较。
Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. In this paper, we consider Craig interpolation for quantifier-free Presburger arithmetic (QFPA). Until recently, quantifier elimination was the only available interpolation method for this theory, which is, however, known to be potentially costly and inflexible. We introduce an interpolation approach based on a sequent calculus for QFPA that determines interpolants by annotating the steps of an unsatisfiability proof with partial interpolants. We prove our calculus to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available Presburger arithmetic benchmarks. The results document the robustness and efficiency of our interpolation procedure. Finally, we compare the procedure against alternative interpolation methods, both for QFPA and linear rational arithmetic.