## Abstractions from Proofs

*
Thomas A. Henzinger,
Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan*

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 *current* values of
variables, and only those which are required 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
variables, 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 *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.

*Proceedings of the
31st Annual Symposium on Principles of Programming Languages*
(POPL), ACM Press, 2004, pp. 232-244.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2004 ACM.