General Interpolation and Strong Amalgamation for Contiguous Arrays

TL;DR

This paper introduces a new theory of contiguous arrays with maxdiff, enabling more expressive array reasoning, and provides an efficient interpolation algorithm that enhances software verification techniques.

Contribution

The paper defines a new array theory with maxdiff, proves its strong amalgamation property, and develops an efficient interpolation algorithm for theory combination.

Findings

The new array theory with maxdiff is more expressive than previous theories.

Models of the theory strongly amalgamate, enabling quantifier-free interpolation.

The proposed algorithm improves existing interpolation methods by reducing complexity.

Abstract

Interpolation is an essential tool in software verification, where first-order theories are used to constrain datatypes manipulated by programs. In this paper, we introduce the datatype theory of contiguous arrays with maxdiff, where arrays are completely defined in their allocation memory and for which maxdiff returns the max index where they differ. This theory is strictly more expressive than the array theories previously studied. By showing via an algebraic analysis that its models strongly amalgamate, we prove that this theory admits quantifier-free interpolants and, notably, that interpolation transfers to theory combinations. Finally, we provide an algorithm that significantly improves the ones for related array theories: it relies on a polysize reduction to general interpolation in linear arithmetics, thus avoiding impractical full terms instantiations and unbounded loops.