Interpolation and the Array Property Fragment

TL;DR

This paper investigates the limitations of interpolation in SMT solvers for the array property fragment, showing that unlike quantifier-free theories, this fragment does not support interpolation, impacting software model checking techniques.

Contribution

The paper proves that the array property fragment does not support interpolation, extending known limitations from EPR to this expressive fragment.

Findings

Array property fragment does not support interpolation.

Supports for interpolation are limited to quantifier-free theories.

Implications for automated software verification methods.

Abstract

Interpolation based software model checkers have been successfully employed to automatically prove programs correct. Their power comes from interpolating SMT solvers that check the feasibility of potential counterexamples and compute candidate invariants, otherwise. This approach works well for quantifier-free theories, like equality theory or linear arithmetic. For quantified formulas, there are SMT solvers that can decide expressive fragments of quantified formulas, e. g., EPR, the array property fragment, and the finite almost uninterpreted fragment. However, these solvers do not support interpolation. It is already known that in general EPR does not allow for interpolation. In this paper, we show the same result for the array property fragment.