Lecturer: James F. Lynch
Office hours: TuTh 10:00AM–11:00AM, 12:15PM–1:00PM, 2:15PM–3:00PM
Lecture hours: TuTh 11:00AM–12:15PM, SC-342
Text: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd Edition,
by Michael R. A. Huth and Mark D. Ryan.
Fundamentals of program specification and verification
(Chapters 1.1–1.5, 2.1–2.4, and 3.1–3.4 in the text).
Abstract State Machines (documentation and software from Division of Foundations of Software Engineering, Microsoft Corporation).
Alloy Analyzer (documentation and software from MIT).
NuSMV Symbolic Model Checker (documentation and software from
If enrollment remains small, then I want to base the grading on homework. This will consist of:
Homework should represent individual effort. While it is permitted (and actually encouraged) to discuss the homework with other students, I expect to see originality in what you turn in. Plagiarism is an infraction of Clarkson regulations and will be penalized.