CS458/558 FORMAL METHODS
SPRING 2005


Lecturer: James F. Lynch
Office: SC-381
Telephone: 268-2374
email: jlynch@clarkson.edu
Office hours: MW 10:00AM-11:00AM and TuTh 9:30AM-11:30AM
Lecture hours: TuTh 8:00AM-9:15M SN-112
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 20)
Homework Assignment 2 (due Thursday January 27)

LAB ASSIGNMENTS


LINKS