Lecturer: James F. Lynch
Office hours: MWF 12:00PM-1:00PM and MW 2:00PM-3:00PM
Lecture hours: MWF 1:00PM-1:50PM SC-346
Text: Logic in Computer Science: Modelling and Reasoning about Systems, Second Edition,
by Michael R. A. Huth and Mark D. Ryan.
Fundamentals of program specification and verification
(Chapters 1, 2, and 3 in the text).
NuSMV Symbolic Model Checker (documentation and software from
Abstract State Machines (documentation and software from Division of Foundations of Software Engineering, Microsoft Corporation).
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.