15-817 Introduction to Model Checking - Main Page

15-817 Introduction to Model Checking

Main Page

Syllabus

Homework
Assignments

Grading

Lecture slides
and Reading

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

Course Description

Announcements

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!

Lectures

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

Contact Information

Professor: Edmund M. Clarke
emc AT cs DOT cmu DOT edu
Office: GHC 9231
Phone: (412) 268-2628
Office hours: By appointment

Teaching Assistant: Will Klieber
wklieber AT cs DOT cmu DOT edu
Office: GHC 7511
Phone: 412-268-2582
Office hours: By appointment

Course Secretary: Denny Marous
dcm AT cs DOT cmu DOT edu
Office: GHC 9229
Phone: 412-268-7660