15-817 Handouts
Date Day Lecture Slides Additional Readings and Notes
9/10ThuTuring Award Lecture (PPT)
9/17ThuBDD Slides C: Chapter 5, pg 51--59
9/24ThuTemporal Logic Slides C: Chapter 3, pg 27--32
10/01ThuTemporal Logic, continued C: Chapter 4, pg 35--39
10/08ThuBasic Fixpoint Theorems
Tarski's Fixed-Point Lemma (updated 2009-10-21 at 11:21)
C: Chapter 6, pg 61--65
10/15ThuSMV Tutorial, Part 1 Cadence SMV tutorial: [ps] [pdf]
Cadence SMV language reference: [html]
Original CMU SMV tutorial: [ps] [pdf]
NuSMV tutorial: [pdf]
10/22ThuSMV Tutorial, Part 2
10/29ThuSymbolic Model Checking
11/05ThuLTL Model Checking by the Tabeau Method C: Section 6.7, pages 87--95
11/12ThuNo class on Nov 12.
11/19ThuPartial Order Reduction
11/26Thu[No class -- Thanksgiving]

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).