A Crash Course on Model Checking - session 2

Опубликовано 25 августа 2016, 20:57

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