Office: 377 Science Center
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.
The homework assignments are due in class on the date posted. There will be a project which will involve verifying a piece of software.