CS 458/558: Formal Methods for Software Verification
Course
Syllabus  Spring 2003
Professor:
Chris Lynch
Office: 377 Science Center
Phone: 2682384
Email:
clynch@clarkson.edu
Office Hours: MW 1012 F 1011
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:
 Logic in Computer Science: Modelling and reasoning
about systems , by Michael R A Huth & Mark D Ryan,
Cambridge University Press, 2002.
 There will be some software that I will download onto
crux for students to use.
Grading Policy:
 2 Exams 60%
 Homeworks and Project 40%
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

Propositional Logic:
Chapter 1
 Verification by Model Checking:
Chapter 3
 Predicate Logic:
Chapters 2
 Verification using Hoare Logic:
Chapter 4
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