Instructor: Prof. Edmund Clarke

Friday 1:30 - 3:00

WeH 4615A

Units: 06

Overview

Logical errors in hardware controllers, communication protocols, and concurrent programs are becoming an increasingly important problem. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. The most widely used method for verifying such systems is based on extensive simulation and can easily miss significant errors when the program is very complicated. Many of these programs can be viewed as having only a finite number of states. When this is the case, an alternative verification technique called "model checking" may be used. In this approach specifications are expressed by automata or temporal logic formulas, and programs are modeled as state transition systems. An efficient search procedure is used to determine automatically if the specifications are satisfied by the transition system. If the specification is not satisfied, a counterexample execution trace is given that shows why the specification is not satisfied..

**POSSIBLE TOPICS TO BE COVERED:**

- Modeling concurrent programs with state transition systems
- Temporal logics
- The mu-calculus and fixpoint theory
- The basic model checking algorithms
- Binary decision graphs and symbolic model checking
- Sat procedures and Bounded Model Checking
- Using Omega-automata to specify properties of concurrent systems
- Notions of equivalence for concurrent systems (observational equivalence, etc)
- Compositional reasoning techniques (e.g. the "assume--guarantee" paradigm)
- Exploiting abstraction and symmetry
- Using induction to reason about systems with many similar processes
- True concurrency and models based on partial orders
- Extending model checking techniques to handle real-time programs
- Model checking techniques for the mu-calculus
- Model Checking for Software and Static Analysis.

Lecture Notes

Date | Topic | Slides/Handout |

01/28/05 | Grand Challenge Problem: Model Check Software | slides |

02/04/05 | Model Checking | slides |

02/11/05 | Boolean Decision Diagrams | exercise files - bdd-example.c hanoi-exercise.c |

02/18/05 | SMV tools | slides, exercises |

02/25/05 | Bounded Model Checking | slides (please ignore the hidden ones) |

03/18/05 | Abstraction in Model Checking | slides |

03/25/05, 04/01/05 |
Partial Order Reduction | slides |

04/08/05 | SPIN | slides (SPIN, SPIN-Tool) |

04/14/05 | LTL Model Checking | slides |

04/22/05 | SAT-based Predicate Abstraction | slides |

04/29/05 | Guest Lecture by Kedar Namjoshi: From Model Checking to Proof Checking |
slides |