We present a process for validating temporal safety properties of
software that uses a well-defined interface. The process requires
only that the user state the property of interest. It then
automatically creates abstractions of C code using iterative
refinement, based on the given property. The process is realized in
the SLAM toolkit, which consists of a model checker, predicate
abstraction tool and predicate discovery tool. We have applied the
SLAM toolkit to a number of Windows NT device drivers to validate
critical safety properties such as correct locking behavior. We have
found that the process converges on a set of predicates powerful
enough to validate properties in just a few iterations.
