The goal of the SLAM project is to analyze system software written in C, and check it against temporal safety properties. The SLAM toolkit uses model checking, program analysis and theorem proving techniques to do automatic analysis, and requires no user-supplied abstractions or annotations such as pre-conditions, post-conditions or loop invariants. 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.

I will start by describing the ideas and algorithms behind SLAM. 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 the second half of the talk, I will detail some of the engineering "secrets" we applied to the basic SLAM process to improve its performance on Windows device drivers.

Bio: Sriram K. Rajamani is a researcher with Microsoft Research. His research interests are in tools and methodologies for building reliable software.

**For more information regarding the talk please contact: Rajeev Alur: http://www.cis.upenn.edu/~alur/home.html