Jakob Rehof

Types as Models: Model Checking Message-Passing Programs

Asynchronous, message-passing programming is becoming increasingly important. However, such programs are notoriously hard to design and test. The goal of the Behave! project is to build tools for checking behavioral properties (like deadlock freedom, invariant checking, message understood properties) of message-passing programs. We want to do this by directly analyzing source code written in an asynchronous programming language.

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).

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.

Host: Ed Clarke
Appointments: Keith LeDonne

Principles of Programming Seminars

POP Seminar
October 26, 2001
3:30 p.m.
Wean Hall 8220