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.


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