15-817 Handouts
Date Day Lecture Slides Additional Readings and Notes
1/12WedTemporal Logic Slides C: Chapter 3, pg 27--32,
C: Chapter 4, pg 35--39
1/19WedBasic Fixpoint Theorems
Tarski's Fixed-Point Lemma
C: Chapter 6, pg 61 - 65
1/26Wed Data Flow Analysis Gary Kildall, “A Unified Approach to Global Program Optimization” (POPL 1973)
1/26WedData Flow Analysis 2 (PPT) (PDF) The Man Who Could Have Been Bill Gates
2/2Wed Data Flow 1 (PPT), Data Flow 2 (PPT)
2/9Wed Data Flow 3 (PPT), Data Flow 4 (PPT)
2/16Wed Model Checking for the Mu Calculus
3/02Wed Marcus du Sautoy: Symmetry
3/09Wed Spring Break
3/16Wed Software Verification using Predicate Abstraction and Iterative Refinement
3/23Wed Abstract Interpretation Cousot's WCC 2004 paper and slides and POPL 1977 paper
3/30Wed Galois Connections
4/05Wed 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).