CS458/558 FORMAL METHODS
Lecturer: James F. Lynch
Office hours: MW
10:00AM-11:00AM and TuTh 9:30AM-11:30AM
Lecture hours: TuTh
Text: Logic in Computer Science: Modelling and
Reasoning about Systems, Second Edition,
by Michael R. A. Huth and Mark
D. Ryan. ISBN: 0-521-54310-X
(The Clarkson bookstore could not get copies of
this book, but it is available from Amazon and Barnes & Noble online.)
SYLLABUS Fundamentals of program specification and
verification (Chapters 1, 2, and 3 in the text).
NuSMV Symbolic Model Checker
(documentation and software from Trento University)
Abstract State Machines
(documentation and software from Division of Foundations of Software
Engineering, Microsoft Corporation).
GRADINGIf 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.
- Written exercises.
- Experience in using actual specification and verification software.
- Possibly a report on a large software project, including what methods were
used, and an analysis of the success or failure of these methods on the
HOMEWORK ASSIGNMENTSHomework Assignment 1 (due
Thursday January 20)
Homework Assignment 2 (due
Thursday January 27)