In hardware and protocol design, behavioral properties are often checked by manually constructing models of the system as communicating finite state machines, and using a model checker to algorithmically explore the state space of the model. Our approach is to use a behavioral type system for extracting models (which are types) from the source code, and perform model checking on the types. We target a source language containing the Pi-calculus. In the most general form, types (models) are CCS processes, and subtyping is a simulation relation on CCS processes.
The talk will describe a new behavioral type system for the Pi-calculus and will include examples of its use in model checking message-passing programs. The talk is based on joint work with Sagar Chaki (CMU) and Sriram K. Rajamani (Microsoft Research).
BIO:
Jakob Rehof is a researcher in the Software Productivity Tools group
at Microsoft Research (Redmond). He joined Microsoft Research in June
1998 after receiving his Ph.D. degree in Computer Science from DIKU,
University of Copenhagen. The current focus of his research is a
project called Behave! with the goal of designing and implementing
tools for checking correctness of concurrent, message-passing
programs. Previous research projects have included scalable
type-based flow analysis, complexity of subtype inference systems,
dynamic typing, and logics for control operators.