The success of model checking for large programs depends crucially on the
ability to efficiently construct parsimonious abstractions.
A predicate abstraction is parsimonious if at each control location, it
specifies only relationships between {\em current} values of variables,
and only those which are {\em necessary} for proving correctness.
Previous methods for automatically refining predicate abstractions until
sufficient precision is obtained do not systematically construct
parsimonious abstractions:
predicates usually contain symbolic constants, and are added heuristically
and often uniformly to many or all control locations at once.
We use Craig interpolation to efficiently construct, from a given abstract
error trace which cannot be concretized, a parsominous abstraction that
removes the trace.
At each location of the trace, we infer the relevant predicates as
an interpolant between the two formulas that define the past and the future
segment of the trace.
Each interpolant is a relationship between current values of program
variables, and is relevant only at that particular program location.
It can be found by a linear scan of the proof of infeasibility of the trace.
We develop our method for programs with arithmetic and pointer expressions,
and call-by-value function calls.
For function calls, Craig interpolation offers a systematic way of
generating relevant predicates that contain only the local variables of
the function and the values of the formal parameters when the function was
called.
We have extended our model checker {\sc Blast} with predicate discovery by
Craig interpolation, and applied it successfully to C programs with more
than 130,000 lines of code, which was not possible with approaches that
build less parsimonious abstractions.
