 |
 |
||
|
|
|
|
 |
 |
|
|
|
|
|
 |
 |
|
|
|
|
|
 |
||
|
|
||
15-817 Handouts
| 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) Graph-Based 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] 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/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 |
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).