15-817A -Introduction to Model Checking
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:

  1. Modeling concurrent programs with state transition systems
  2. Temporal logics
  3. The mu-calculus and fixpoint theory
  4. The basic model checking algorithms
  5. Binary decision graphs and symbolic model checking
  6. Sat procedures and Bounded Model Checking
  7. Using Omega-automata to specify properties of concurrent systems
  8. Notions of equivalence for concurrent systems (observational equivalence, etc)
  9. Compositional reasoning techniques (e.g. the "assume--guarantee" paradigm)
  10. Exploiting abstraction and symmetry
  11. Using induction to reason about systems with many similar processes
  12. True concurrency and models based on partial orders
  13. Extending model checking techniques to handle real-time programs
  14. Model checking techniques for the mu-calculus
  15. 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