The SLAM project at Microsoft Research has created an automated process for finding errors in C programs, driven by a user-supplied (temporal safety) property. The process requires only that the user state the property of interest. It then automatically creates and analyzes abstractions of the C code, based on given property. The process is realized in the SLAM toolkit, which has tools to automatically create, analyze and refine abstract models of C code. The toolkit iteratively refines the model until it is precise enough to find a true defect or to validate the given property. We have applied the SLAM toolkit to numerous Windows XP device drivers to validate critical safety properties such as correct locking behavior, which I will report on here.

About Thomas Ball

Thomas Ball is a 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 reliability of software. He is currently working on the SLAM project at Microsoft Research, with the goal of automatically checking properties of software interfaces. Previous to Microsoft, he was a researcher at Bell Laboratories from 1993 to 1999. He received his B.A. in computer science from Cornell University in 1987 and his Masters and Ph.D. in computer science in 1990 and 1993 from the University of Wisconsin-Madison. For more information, see http://research.microsoft.com/~tball/.

Tuesday, Sept. 25 at 4pm in DH 1064

A reception will precede the talk at 3:30pm - Location: TBA