Bug Catching: Automated Program Verification

Course Overview

High-profile bugs continue to plague the software industry, leading to major problems in the reliability, safety, and security of systems. This course teaches students how to write bug-free code through the process of software verification, which aims to prove the correctness of a program with respect to a mathematical specification. Along the way, students will learn how to:

Students will learn the principles and algorithms behind automated verification tools, and understand their practical limitations while gaining experience writing verified, machine-checked code that solves real problems.

Lectures: Tue Thu 12:30-1:50pm, HH B131


Matt Fredrikson mfredrik@cmu OH: Fridays @ 3pm CIC 2126


Myra Dotzel mdotzel@andrew OH: Tuesdays @ 10am GHC 9223
Cole Ramos jcramos@andrew OH: Thursdays @ 3pm CIC 2214
Joseph Reeves jereeves@andrew OH: Wednesday @ 2pm GHC Table 3

Piazza: piazza.com/cmu/spring2023/15414

Gradescope: www.gradescope.com/courses/353280

Software: This course will teach students how to use the Why3 deductive verification platform. See the notes on installation and editing.


Welcome to Spring 2023! Be sure to check you are enrolled in Gradescope and Piazza. 1/17/2023