15-817 Introduction to Model Checking
|
|
|
Main
Page
|
|
|
|
|
Syllabus
|
Assignments
|
|
|
|
Grading
|
Reading
|
|
|
Professor
|
|
15-817 Handouts
| Date |
Day |
Lecture Slides |
Additional Readings and Notes |
| 1/12 | Wed | Temporal Logic Slides |
C: Chapter 3, pg 27--32,
C: Chapter 4, pg 35--39
|
| 1/19 | Wed | Basic Fixpoint Theorems
Tarski's Fixed-Point Lemma
| C: Chapter 6, pg 61 - 65
|
| 1/26 | Wed |
Data Flow Analysis
|
Gary Kildall, “A Unified Approach to Global Program Optimization” (POPL 1973)
|
| 1/26 | Wed | Data Flow Analysis 2
(PPT)
(PDF)
|
The Man Who Could Have Been Bill Gates
|
| 2/2 | Wed |
Data Flow 1 (PPT),
Data Flow 2 (PPT)
|
|
| 2/9 | Wed |
Data Flow 3 (PPT),
Data Flow 4 (PPT)
|
|
| 2/16 | Wed |
Model Checking for the Mu Calculus
|
|
| 3/02 | Wed |
Marcus du Sautoy: Symmetry
|
|
| 3/09 | Wed |
Spring Break
|
|
| 3/16 | Wed |
Software Verification using Predicate Abstraction and Iterative Refinement
|
|
| 3/23 | Wed |
Abstract Interpretation
|
Cousot's WCC 2004 paper and slides and POPL 1977 paper
|
| 3/30 | Wed |
Galois Connections
|
|
| 4/05 | Wed |
SMV Tutorial, Part 0
SMV Tutorial, Part 1
SMV Tutorial, Part 2
Note: In the conditional expression 'case': if all the conditions are false, then the result of the expression is undefined (i.e., equivalent to a nondeterministic choice).
|
Cadence SMV tutorial: [ps]
[pdf]
Cadence SMV language reference: [html] [ps]
Original CMU SMV tutorial: [ps]
[pdf]
NuSMV tutorial: [pdf]
|
15-817 Textbooks:
- C: Model Checking
by Edmund M. Clarke, Orna Grumberg, and Doron Peled. (1999, MIT Press).
- B: Principles of Model Checking
by Christel Baier and Joost-Pieter Katoen. (2008, MIT Press).
|
