CS458/558 FORMAL METHODS
Lecturer: James F. Lynch
Office hours: TuTh 10:45AM-12:00PM and 1:15PM-2:30PM
Lecture hours: TuTh 9:30AM-10:45AM SC-354
Text: Logic in Computer Science: Modelling and Reasoning about
Systems, by Michael R. A. Huth and Mark D. Ryan
Fundamentals of program specification and verification (Chapters 1, 2,
and 3 in the text).
Case studies of successful and unsuccessful software projects (other sources).
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:
- Written exercises.
- A report on a large software project, including what methods were
used, and an analysis of the success or failure of these methods on
- Specifying or verifying software using methods covered in the course.