CS 458/558: Formal Methods for Software Verification
Course Syllabus -- Spring 2003

Professor: Chris Lynch
Office: 377 Science Center
Phone: 268-2384
E-mail: clynch@clarkson.edu

Office Hours: MW 10-12 F 10-11

Course Objective: This course will teach formal methods of specifying and verifying software. It will discuss ways of using logic to express properties of programs, and how to prove the correctness of those properties. The main methods dicussed will be model checking and Hoare logic. At the end of the course, students will be able to use these two methods for specifying and verifying software. But more generally, they will have an understanding of what it means to formally prove a program's correctness, and hopefully an idea of when it is appropriate to use these techniques.

Text:

Grading Policy:

The homework assignments are due in class on the date posted. There will be a project which will involve verifying a piece of software.

Course Outline

Chapters 2 and 4 cover the important material of the course, and will be covered thoroughly, possibly using material ouside of the book. Chapters 1 and 3 are needed as background, and I assume that students have seen those topics before.
Last modified: 9 Januuary 2003
clynch@clarkson.edu