Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)

TL;DR

This paper explores interpolation in extended Presburger arithmetic theories, showing limitations of quantifier-free methods and proposing fragments with effective interpolation and a sound procedure for array theories.

Contribution

It introduces new interpolation procedures for extended Presburger theories and identifies fragments with effective interpolation, advancing program verification techniques.

Findings

Quantifier-free interpolation is impossible for certain Presburger extensions.

Fragments with guarded quantification are closed under interpolation.

A sound interpolation procedure for array theories with potential quantifiers.

Abstract

Craig interpolation has emerged as an effective means of generating candidate program invariants. We present interpolation procedures for the theories of Presburger arithmetic combined with (i) uninterpreted predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii) extensional arrays (QPA+AR). We prove that none of these combinations can be effectively interpolated without the use of quantifiers, even if the input formulae are quantifier-free. We go on to identify fragments of QPA+UP and QPA+UF with restricted forms of guarded quantification that are closed under interpolation. Formulae in these fragments can easily be mapped to quantifier-free expressions with integer division. For QPA+AR, we formulate a sound interpolation procedure that potentially produces interpolants with unrestricted quantifiers.