Electronic Systems Design Seminar
http://embedded.eecs.berkeley.edu/esd-seminar

Model Checking, Program Analysis and Theorem Proving: Kitchen Sink? Dr. Sriram Rajamani Microsoft Research Monday, October 15, 2001, 1:00-2:00pm 540AB Cory Hall (DOP Center Classroom)

Abstract

Property checking provides a way to partially validate software. In this approach, the user provides a set of properties that the code should satisfy, and tools are provided to check if the code satisfies these properties. Recently, there has been a confluence of ideas from Model Checking, Program Analysis and Theorem Proving to build such checking tools.

In this talk, we will outline the roles played by each of these techniques using experiences from two projects at Microsoft Research:

• The SLAM project (http://research.microsoft.com/slam, joint work with Thomas Ball), where we check C programs with structures, pointers and procedures against temporal specifications using a model checker (bebop), a predicate abstraction tool (c2bp) and a predicate discovery tool (newton). I will present experiences in applying SLAM to Windows NT device drivers.
• The BEHAVE! project (http://research.microsoft.com/behave, joint work with Jakob Rehof), where we use a type system to extract behavioral types from message passing programs, and use model checking on the behavioral types. 

Speaker

I am a researcher with Microsoft Research. I currently work on tools and techniques for building reliable software. I joined Microsoft Research in 1999. I am an alumnus of the CAD group at Berkeley (where I completed a PhD thesis titled: “New directions in refinement checking”). Before becoming a researcher, I worked in product groups and shipped products (for over 5 years) with Xilinx Inc, San Jose, CA and Syntek Systems Inc, Bethesda, MD. Someday, I plan to write a bio without using parentheses.