Polymorphic Predicate Abstraction
ACM Transactions on Programming Languages and Systems (TOPLAS), 27(2):314-343, March 2005.
Thomas Ball, Todd Millstein, Sriram Rajamani
Predicate abstraction is a technique for creating abstract models of
software that are amenable to model checking algorithms. We show how
polymorphism, a well-known concept in programming languages and
program analysis, can be incorporated in a predicate abstraction
algorithm for C programs. The use of polymorphism in predicates, via
the introduction of symbolic names for values, allows us to model the
effect of a procedure independent of its calling contexts. Therefore,
we can safely and precisely abstract a procedure once and then reuse
this abstraction across multiple calls and multiple applications
containing the procedure. Polymorphism also enables us to handle
programs that need to be analyzed in an open environment, for all
possible callers. We have proved that our algorithm is sound and have
implemented it in the C2BP tool as part of the SLAM software model
checking toolkit.
[PDF]