Date: September 4, 2002
Location: 3305 Newell-Simon Hall
Time: 1:30-3:00 pm

Abstract: The goal of the SLAM project is to validate sequential C programs against temporal safety properties. The toolkit does not require program annotation (invariants are inferred) and minimizes noise (false error messages) through a process known as `counterexample-driven refinement''.

We have successfully applied the SLAM toolkit to over 100 Windows device drivers, to both validate their behavior and find defects in their usage of kernel-level APIs. The SLAM toolkit currently is in transition from a research prototype to a product-grade tool that will be supported and used by the Windows development organization.

As is often the case, there is a gap between the theory and algorithms one publishes and the implementation of a tool that has been engineered to perform acceptably in practice. In this talk, I will detail some of the engineering "secrets" we applied to the basic SLAM process to improve its performance on Windows device drivers.

(Joint work with Sriram K. Rajamani, Westley Weimer and Satyaki Das)