Model checking is a technique to find bugs in systems by systematically exploring their state spaces. Due to state space explosion, model checkers typically operate on a manually constructed finite-state abstraction of the system. The goal of the SLAM project is to model check software written in common programming languages directly. SLAM has been successfully used to find and fix errors in Windows device drivers written in the C language.
SLAM operates by automatically constructing and refining model-checkable abstractions (called Boolean Programs) of a C program. The first part of this tutorial will describe how the SLAM project has combined and extended results from the areas of program analysis, model checking and theorem proving to analyze critical properties of systems software written in the C language. The second half of the tutorial will present some of the engineering "secrets" we applied to the basic SLAM process to improve its performance on Windows device drivers.
SLAM is joint work with Byron Cook, Vladimir Levin and Jakob Lichtenberg, who have been instrumental in helping us transfer the SLAM technology to Microsoft's Windows division.
Thomas Ball is a Senior Researcher in the Software Productivity Tools group at Microsoft Research. His research interests are in how combinations of program analysis, model checking and theorem proving techniques can help improve the correctness and reliability of programs. He has been at Microsoft Research since 1999, primarily working on the SLAM project. Previous to Microsoft, he was in the Software Production Research Department of Bell Laboratories. He received his Ph.D. in Computer Science in 1993 from the University of Wisconsin-Madison.
Sriram K. Rajamani is a Researcher with the Software Productivity Tools group at Microsoft. Sriram came to MSR in Fall 1999 and started the SLAM project along with Thomas Ball. More recently, Sriram has been also working on the Behave! project with Jakob Rehof and James Larus. Sriram's goals are to use formal methods such as model checking, theorem proving and program analysis to greatly improve the lives of programmers, and improve the reliability of software they write. Sriram knows his customers. Prior to becoming a researcher, he worked as a programmer for over 5 years, for Xilinx Inc in San Jose, CA and Syntek Systems Inc in Bethesda, MD. Sriram received a Ph.D. in Computer Science from the University of California at Berkeley.