Computer Science Department Logo
15-817 Introduction to Model Checking
Main Page
  
Main Page 
 
Lecture Schedule, Notes and Readings
Assignments, Exams and Solutions
 Syllabus
Assignments
Grading and Policies
Textbook and Other Resources
Grading 
Reading 
Professor
Professor 
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]
12/03Thu

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