Automatically Validating Temporal Safety Properties of Interfaces
Thomas J. Ball, Sriram K. Rajamani · 2001
Abstract. We present a process for validating temporal safety proper-ties of software that uses a well-dened interface. The process requires only that the user state the property of interest. It then automatically creates abstractions of C code using iterative renement, based on the given property. The process is realized in the SLAM toolkit, which con-sists of a model checker, predicate abstraction tool and predicate discov-ery 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. 1