Date 
Day 
Lecture Slides 
Additional Readings and Notes 
9/11  Thu 
Birth of Model Checking (
[ppt],
[pdf],
[pdf 4up] ) 

9/18  Thu 
Birth of Model Checking, continued 

9/25  Thu 
Symbolic Model Checking with BDDs (pdf) 
Efficient Implementation of a BDD Package by Randy Bryant et al (1991)
GraphBased Algorithms for Boolean Function Manipulation by Randy Bryant (1986) (revised ver.) 
10/02  Thu 
Symbolic Model Checking with BDDs (continued) [pdf] 

10/09  Thu 
Using the SMV Model Checker
(ppt)
(pdf)
Peterson's Mutex Algorithm [pdf]
oct09smvfiles.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/16  Thu 
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/23  Thu 
Turing Award Lecture in Wean 7500 (doors open at 3:30 pm; lecture begins at 4:00 pm). 

10/30  Thu 
CTL* Logic
Kripke structure for which ((A F G p) != (AF AG p)) 

11/06  Thu 
Review of Bounded Model Checking 

11/13  Thu 
Partial Order Reduction [pdf] 
State Space Reduction using Partial Order Techniques by Clarke, Grumberg, Minea, and Peled

11/20  Thu 
(No class) 

11/27  Thu 
Thanksgiving holiday  No class 
