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 both large and small. Software verification aims to prove the correctness of a program with respect to a precise specification, and is an effective way to find and prevent such bugs. Building on several decades of research, this area has produced highly-automated tools and techniques that can be brought to bear in practice. This course will cover the following topics:

Students will learn the principles and algorithms behind automated verification tools, and understand their practical limitations. Along the way, they will gain experience writing verified, machine-checked software by implementing some of these techniques and applying state-of-the-art tools to prove that their code is free of bugs.

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

Instructors: Matt Fredrikson and André Platzer

TAs: Jonathan Laurent, Tianyu Li

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


There will be a work session for Lab 1 on 9/22 at 4pm in GHC 6501. 9/21/17
Lab 1 assigned, due on 10/6. 9/21/17
Homework 4 assigned, due on 9/28. 9/21/17
Homework 3 assigned, due on 9/21. 9/14/17
Correction to Homework 2, Problem 5. Please check the current handout for the up-to-date version. 9/11/17
Homework 2 and Lab 0 assigned, due on 9/14. 9/7/17
Homework 1 assigned, due on 9/7. 8/31/17