Craig interpolation has become a versatile tool in formal
verification, in particular for generating intermediate assertions in
safety analysis and model checking. In this paper, we present a novel
interpolation procedure for the theory of arrays, extending an
interpolating calculus for the full theory of quantifier-free
Presburger arithmetic, which will be presented at IJCAR this year. We
investigate the use of this procedure in a software model checker for
C programs. A distinguishing feature of the model checker is its
ability to faithfully model machine arithmetic with an encoding into
Presburger arithmetic with uninterpreted predicates. The interpolation
procedure allows the synthesis of quantified invariants about
arrays. This paper presents work in progress; we include initial
experiments to demonstrate the potential of our method.