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.

Contact the staff: 15414-staff@lists.andrew.cmu.edu

Instructor: Matt Fredrikson

TAs: Di Wang, Ryan Chen

Lectures: TuTh 12:00-1:20pm in GHC 4307.


Homework 6 released for extra credit, and is due on 5/1 at 11:59pm 4/22/20
Homework 5 released, and is due on 4/17 at 11:59pm 4/9/20
Lab 4 released, and is due on 5/1 at 11:59pm. There is a mandatory checkpoint on 4/20. 4/4/20
Homework 4 released, and is due on 4/5 at 11:59pm. 3/25/20
The first SAT lab has been released, and is due on 4/2 at 11:59pm. 2/23/20
Lab 2 has been released, and is due on 3/10 at 11:59pm. 2/23/20
Homework 3 has been released, and is due on 2/23 at 11:59pm. 2/12/20
Lab 1 has been posted, and is due on 2/18 at 11:59pm. 2/3/20
Homework 2 has been posted, and is due on 2/4 at 11:59pm. 1/23/20
Homework 1 and Lab 0 have been posted. Homework 1 is due at 11:59pm on 1/23, and Lab 0 is due at 11:59 on 1/30. 1/16/20
Welcome to Spring 2020! Be sure to enroll in the Gradescope section with entry code MJ8Z24, and sign up for the Piazza section. 1/14/20