Model Checking, Program Analysis and Theorem Proving: Kitchen
Sink?
Sriram Rajamani,
Microsoft Research
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 (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)
- The BEHAVE! project (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.