15-817 Handouts
Date Day Lecture Slides Additional Readings and Notes
9/11Thu Birth of Model Checking ( [ppt], [pdf], [pdf 4up] )  
9/18Thu Birth of Model Checking, continued  
9/25Thu Symbolic Model Checking with BDDs (pdf) Efficient Implementation of a BDD Package by Randy Bryant et al (1991)

Graph-Based Algorithms for Boolean Function Manipulation by Randy Bryant (1986) (revised ver.)

10/02Thu Symbolic Model Checking with BDDs (continued) [pdf]  
10/09Thu Using the SMV Model Checker (ppt) (pdf)
Peterson's Mutex Algorithm [pdf]
oct09-smv-files.zip
Running Cadence SMV on the CMU Andrew machines
Cadence SMV tutorial: [ps] [pdf] [html]
Cadence SMV language reference: [html]
Original CMU SMV tutorial: [ps] [pdf]
NuSMV tutorial: [pdf]
10/16Thu Symbolic Model Checking with SAT [pdf] Computational Challenges in Bounded Model Checking by Clarke, Kroening, Ouaknine, and Strichman

Symbolic Model Checking without BDDs by Biere, Cimatti, Clarke, and Zhu

10/23Thu Turing Award Lecture in Wean 7500 (doors open at 3:30 pm; lecture begins at 4:00 pm).
10/30Thu CTL* Logic
Kripke structure for which ((A F G p) != (AF AG p))
11/06Thu Review of Bounded Model Checking
11/13Thu Partial Order Reduction [pdf] State Space Reduction using Partial Order Techniques by Clarke, Grumberg, Minea, and Peled
11/20Thu (No class)
11/27Thu Thanksgiving holiday -- No class

15-817 Textbooks:

  • Model Checking by Edmund M. Clarke, Orna Grumberg, and Doron Peled. (1999, MIT Press).
  • Principles of Model Checking by Christel Baier and Joost-Pieter Katoen. (2008, MIT Press).