CS458/558 FORMAL METHODS
SPRING 2004


Lecturer: James F. Lynch
Office: SC-381
Phone: 268-2374
E-mail: jlynch@clarkson.edu
Office hours: MW 10:00AM-11:00AM and TuTh 9:30AM-11:30AM
Lecture hours: MWF 8:00-8:50 a.m.
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).

GRADING

If enrollment remains small, then I want to base the grading on homework. This will consist of:
  1. Written exercises.
  2. Experience in using actual specification and verification software.
  3. 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 project.
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.

HOMEWORK ASSIGNMENTS

Homework Assignment 1 (due Thursday January 22)
Homework Assignment 2 (due Thursday January 29)

LAB ASSIGNMENTS


LINKS