Refining Approximations in Software Predicate Abstraction

Predicate abstraction is an automatic technique that can be used to find abstract models of large or infinite-state systems. In tools like SLAM, where predicate abstraction is applied to software model checking, a number of heuristic approximations must be used to improve the performance of computing an abstraction from a set of predicates. For this reason, SLAM can sometimes reach a state in which it is not able to further refine the abstraction. In this paper we report on an application of Das & Dill's algorithm for predicate abstraction refinement. SLAM now uses this strategy lazily to recover precision in cases where the abstractions generated are too coarse. We describe how we have extended Das & Dill's original algorithm for use in software model checking. Our extension supports procedures, threads, and potential pointer aliasing. We also present results from experiments with SLAM on device driver sources from the Windows operating system.