CS 458/558: Formal Methods for Software Verification
Syllabus -- Spring 2003
Office: 377 Science Center
Office Hours: MW 10-12 F 10-11
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.
- 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.
- 2 Exams 60%
- Homeworks and Project 40%
are due in class on the date posted.
There will be a project which will involve
verifying a piece of software.
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.
- Verification by Model Checking:
- Predicate Logic:
- Verification using Hoare Logic:
Last modified: 9 Januuary 2003