B.U.G. Logo 15-817 Introduction to Model Checking
Fall 2009 Semester
Computer Science Department

Course Description


  • Class for Nov 12 is cancelled.
  • For Assignment 3b, you only need to prove the weaker version ({z | T(z) ⊆ z} instead of {z | T(z) = z}}.
  • If you have having trouble with DumpDot, try using the updated version of cudd-assignment.cc.
  • To compile CUDD using the 64-bit version of gcc, you may need to change the XCFLAGS line Makefile. For example:
        XCFLAGS = -m32 -malign-double -DHAVE_IEEE_754 -DBSD
  • Welcome to 15817!


Thursdays from 3:00-4:20pm in GHC 5222.

Contact Information

Professor: Edmund M. Clarke
e­mc A­T c­s DOT cmu DOT e­du
Office: GHC 9231
Phone: (412) 268-2628
Office hours: By appointment
Teaching Assistant: Will Klieber
w­klieber A­T c­s DOT cmu DOT e­du
Office: GHC 7511
Phone: 412-268-2582
Office hours: By appointment
Course Secretary: Denny Marous
d­cm AT c­s DOT cmu DOT e­du
Office: GHC 9229
Phone: 412-268-7660