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.

Spring 2022: This course is SYNCHRONOUS REMOTE at least for the first two weeks of classes, using the ohyay platform for live lectures
Please check out the ohyay platform tips and login instructions before the first lecture
When we are back to in-person expectation (IPE) we will be in Hamerschlag Hall B131

Lectures: Tue Thu 11:50-1:10pm, 15-414 Ohyay Course Space then HH B131

Lecture Recordings: Will be available on YouTube YouTube Channel

Office Hours Locations: Either in-person only or hybrid in-person + Ohyay. See Calendar and Map of GHC5 Spaces


Matt Fredrikson mfredrik@cmu Mon 1:30pm-3:00pm
Frank Pfenning fp@cs Wed 12:00pm-1:30pm


May Li mayli@andrew Tue 3:00pm-4:30pm
Warwick Marangos wmarango@andrew Wed 5:00pm-6:30pm
Long Pham longp@andrew Fri 3:00pm-4:30pm
Victor Song yiwenson@andrew Mon 7:00pm-8:30pm

Piazza: piazza.com/cmu/spring2022/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 2022! Be sure to check you are enrolled in Gradescope and Piazza. 1/12/2022