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

Course Description


  • Mon Dec 1: Homework 2 posted.
  • Wed Nov 19: Reminder: there is no class this week.
  • Mon Nov 10: For Part 4 of Homework 1, please print out your SMV file and turn it in during class. You do not need to turn in an electronic copy.  Please also make an effort to do Part 5 as best you can. (Part 5 is the problem that Ed mentioned in class; it was not on the original printout, but it is on the electronic version of Homework 1.) If you are unable to completely do this problem, please turn in your work; this problem will be graded leniently.
  • Sat Nov 1: Hints for Part 5 have been added to Assignment 1.
  • Fri Oct 31: Assignment 1 is now available. Parts 1, 2, and 3 are due Nov 6.


Thursdays from 3:00-4:20pm in Wean Hall Rm 4623.

Contact Information

Professor: Edmund M. Clarke
e​mc A​T c​s DOT cmu DOT e​du
Office: Wean Hall Rm 7117
Phone: (412) 268-2628    Fax: (412) 268-5576 
Office hours: By appointment
Teaching Assistant: Will Klieber
w​klieber A​T c​s DOT cmu DOT e​du
Office: Wean Hall Rm 3713
Phone: 412-268-5944
Office hours: By appointment
Course Secretary: Denny Marous
d​cm AT c​s DOT cmu DOT e​du
Office: Wean Hall Rm 7116
Phone: (412) 268-7660 Fax: (412) 268-5576