FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Efficient Interpolation for the Theory of Arrays

Authors: Jochen Hoenicke and Tanja Schindler

Paper Information

Title:Efficient Interpolation for the Theory of Arrays
Authors:Jochen Hoenicke and Tanja Schindler
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:Satisfiability Modulo Theory, Craig Interpolation, Quantifier-free Theory of Arrays
Abstract:

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.

Pages:16
Talk:Jul 14 11:00 (Session 95F: SMT 1)
Paper: