Interpolation based automatic abstraction is a powerful and robust
technique for the automated analysis of hardware and software systems.
In this talk we present a general algorithm to construct interpolants
for any recursively enumerable theory. In particular, efficient
procedures to construct interpolants for the theories of arrays, sets,
and multisets are discussed using the reduction approach for obtaining
decision procedures for complex data structures. The approach taken
is that of reducing the theories of such data structures to the
theories of equality and linear arithmetic for which efficient
interpolating decision procedures exist. This enables interpolation
based techniques to be applied to programs that manipulate these data