Rewriting-based Quantifier-free Interpolation for a Theory of Arrays

Roberto Bruttomesso, Silvio Ghilardi & Silvio Ranise
The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier-free interpolants in general. In this paper, we show that, with a minor extension to the theory of arrays, it is possible to obtain quantifier-free interpolants. We prove this by designing an interpolating procedure, based...