An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic |
| |
Authors: | Angelo?Brillout Daniel?Kroening Email author" target="_blank">Philipp?RümmerEmail author Thomas?Wahl |
| |
Affiliation: | 1.ETH Zurich,Zurich,Switzerland;2.Computer Science Department,Oxford University,Oxford,UK;3.Department of Information Technology,Uppsala University,Uppsala,Sweden |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|