15-817 Introduction to Model Checking - Textbook, handouts and other resources

[画像:Computer Science Department Logo]

15-817 Introduction to Model Checking

Main Page

Lecture Schedule, Notes and Readings

Assignments, Exams and Solutions

Syllabus

Assignments

Grading and Policies

Textbook and Other Resources

Grading

Reading

Professor

15-817 Handouts

Date Day Lecture Slides Additional Readings and Notes

9/10 Thu Turing Award Lecture (PPT)

9/17 Thu BDD Slides C: Chapter 5, pg 51--59

9/24 Thu Temporal Logic Slides C: Chapter 3, pg 27--32

10/01 Thu Temporal Logic, continued C: Chapter 4, pg 35--39

10/08 Thu Basic Fixpoint Theorems
Tarski's Fixed-Point Lemma (updated 2009年10月21日 at 11:21) C: Chapter 6, pg 61--65

10/15 Thu SMV Tutorial, Part 1 Cadence SMV tutorial: [ps] [pdf]
Cadence SMV language reference: [html]
Original CMU SMV tutorial: [ps] [pdf]
NuSMV tutorial: [pdf]

10/22 Thu SMV Tutorial, Part 2

10/29 Thu Symbolic Model Checking

11/05 Thu LTL Model Checking by the Tabeau Method C: Section 6.7, pages 87--95

11/12 Thu No class on Nov 12.

11/19 Thu Partial Order Reduction

11/26 Thu [No class -- Thanksgiving]

12/03 Thu

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