15-817 Introduction to Model Checking Fall 2009 Semester Computer Science Department

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

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