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

Instructors: Matt Fredrikson and Ruben Martins

TAs: Krishna Bagadia, Rameel Rizvi

Lectures: TuTh 10:30-11:50am in GHC 4211.


Lab 4 assigned. First checkpoint on 11/27, final due date 12/4. 11/13/18
Lab 3 assigned, due Tuesday 11/13. 11/2/18
Lab 2 assigned, due Friday 11/2. 10/18/18
Homework 5 assigned, due Sunday 10/7. 9/28/18
Lab 1 assigned, due Tuesday 10/9. 9/25/18
Homework 4 assigned, due Thursday 9/27 Friday 9/28 (1 day extension due to TOC). 9/20/18
Homework 3 (due Thursday 9/20) and Lab 0 (due Friday 9/21) assigned. 9/13/18
Homework 2 assigned, due 9/13. 9/6/18
First homework assigned, due 9/6. 8/30/18
The course website for the Fall 2017 offering can be found here. 8/26/18