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.

Lectures: Tue Thu 12:30-1:50pm, HH B131


Ruben Martins rubenm@andrew.cmu.edu OH: Wednesdays @ 2pm GHC 7129


Map of GHC5 Spaces for OH

Cayden Codel ccodel@andrew.cmu.edu OH: Fridays @ 1.30pm GHC5 Table 2
Pratap Singh prataps@andrew.cmu.edu OH: Mondays @ 3pm CIC 2201
Tony Yu tonyy@andrew.cmu.edu OH: Thursdays @ 5pm GHC5 Carrel 1
Ying Sun yingsun@andrew.cmu.edu OH: Tuesdays @ 2pm GHC5 Table 4

Piazza: piazza.com/cmu/spring2023/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.


Mini-Project 1 has been posted. The checkpoint is due at 11:59 pm on 2/23 and the final submission is due at 11:59 pm on 3/1. 2/16/2024
Assignment 3 has been posted and is due at 11:59pm on 2/16. 2/9/2024
Assignment 2 has been posted and is due at 11:59pm on 2/9. 2/2/2024
Assignment 1 has been posted and is due at 11:59pm on 2/2. 1/26/2024
Assignment 0 has been posted and is due at 11:59pm on 1/26. 1/19/2024
Welcome to Spring 2024! Be sure to check you are enrolled in Gradescope and Piazza. 1/16/2024