A Crash Course on Model Checking – session 1

Title: A Crash Course on Model Checking
Date: Three Sessions: 10/28/99, 11/4/99, 11/11/99
Description:
In recent years, model checking has been widely successful in finding bugs in hardware design, and protocol design. There have been recent attempts (in the past two years) in applying model checking to improve software reliability. This course is a tutorial introduction to model checking.

We will start with models, specification logics, and the model checking problem, which is to check if a formula holds in a model. We will survey model checking algorithms for different kinds of temporal logics. Then, we will study the state-explosion problem that arises in model construction, and various techniques to handle state-explosion (including binary decision diagrams, partial order methods, symmetry, assume-guarantee, and abstractions). We will conclude with a survey of what has been tried in applying model checking to software.

Prerequisites: None

Reading Materials: None

Speaker Details

I am Assistant Managing Director of Microsoft Research India, and “area champion” for two research areas in Microsoft Research India: (1) Programming Languages and Tools, (2) Security and Privacy

I am broadly interested in programming languages and tools to improve software productivity. Specific current research interests include: building new programming tools by combining verification, testing, and statistics, designing new programming models for concurrent and distributed systems, and designing programming languages and analysis techniques to enable widespread use of machine learning by non-experts.

I moved to MSR India towards the end of 2005. Prior to moving to MSR India, I was manager for the Software Productivity Tools (SPT) group at MSR Redmond. SPT was a truly remarkable set of people.

Date:
Speakers:
Sriram Rajamani
Affiliation:
Microsoft Corp

Watch Next