Polymorphic Predicate Abstraction

Predicate abstraction is a technique for creating abstract models of software that are amenable to model checking algorithms. Because model checking algorithms have worst-case behavior that is exponential in the number of predicates in the model, it is highly desirable to reduce the number of predicates, while retaining precision. 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 large number of monomorphic predicates equivalently with a small number of polymorphic predicates. Polymorphic predicate abstraction of C programs is complicated by the presence of procedures and pointers, and our algorithm handles both constructs. We have proved that our algorithm is sound and have implemented it in the C2BP tool.