CS458/558 FORMAL METHODS FOR PROGRAM VERIFICATION
SPRING 2009


Lecturer: James F. Lynch
Office: SC-381
Telephone: 268-2374
email: jlynch@clarkson.edu
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.
ISBN: 0-521-54310-X


SYLLABUS

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 Trento University)


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 listed above.

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)

 


SUGGESTED PROJECTS

 


LINKS