15-819B Specification, Verification, and Model Checking

("Spec and Check!")

(12 units) Spring 2004

Edmund M. Clarke and John C. Reynolds

Tuesdays and Thursdays, 1:30-2:50 pm Wean Hall 4615A

Course Description

This course will focus on two of the most successful approaches to verification: Hoare Logic and Temporal Logic Model Checking. The goal will be to teach students how to construct proofs in Hoare Logic and how to use Model Checking tools. Examples will come mainly from software and protocol verification.

PREREQUISITES: The course is designed to be mostly self-contained. In particular, a prior logic course is not assumed. Knowledge of programming languages and concurrency (at the undergraduate level) will be helpful. Although Model Checking is useful for hardware verification, no knowledge of computer hardware will be required for this course.


(1) Logic in Computer Science: Modeling and Reasoning about Systems by M. Huth and M. Ryan

(2) Model Checking by E. M. Clarke, Orna Grumberg, and Doron Peled

METHOD OF EVALUATION: Grading will be based on a set of assignments and a course project.


Course Notes (in Postscript)

Minor corrections have been made to some of these notes since they were passed out in class. This is indicated by a more recent revision date.

Homework Assignments (in Postscript)

Last updated: April 1, 2004