Efficient Interpolation for the Theory of Arrays

TL;DR

This paper introduces a new efficient interpolation method for the theory of arrays using proof tree preservation and weak equivalence, improving the process of generating interpolants for memory safety verification in C programs.

Contribution

The paper presents a novel interpolation algorithm based on proof tree preservation and weak equivalence, addressing inefficiencies in existing array interpolation techniques.

Findings

Interpolants have worst-case exponential size for extensionality lemmas.

Interpolants have worst-case quadratic size for other lemmas.

The approach effectively proves memory safety in C programs.

Abstract

Existing techniques for Craig interpolation for the quantifier-free fragment of the theory of arrays are inefficient for computing sequence and tree interpolants: the solver needs to run for every partitioning $(A, B)$ of the interpolation problem to avoid creating $AB$-mixed terms. We present a new approach using Proof Tree Preserving Interpolation and an array solver based on Weak Equivalence on Arrays. We give an interpolation algorithm for the lemmas produced by the array solver. The computed interpolants have worst-case exponential size for extensionality lemmas and worst-case quadratic size otherwise. We show that these bounds are strict in the sense that there are lemmas with no smaller interpolants. We implemented the algorithm and show that the produced interpolants are useful to prove memory safety for C programs.