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:

Specify correct program behavior
Prove the correctness of their code
Use formal semantics to reason about the soundness of proof rules
Write practical and efficient verified code
Use decision procedures and model checkers to reduce verification effort

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.

Spring 2021: This course is REMOTE ONLY, using the ohyay platform for live lectures
Please check out the ohyay platform tips and login instructions before the first lecture

Lectures: Tue Thu 12:20-1:40pm, 15-414 Ohyay Course Space

Lecture Recordings: YouTube Channel

Office Hour Location: 15-414 Ohyay Course Space

Instructors:

Ruben Martins, rubenm@andrew, Mon 1-3pm
Frank Pfenning, fp@cs, Wed 12-1pm and Fri 10-11am

TAs:

Jatin Arora, jatina@andrew, Thu 6-8pm
Aditi Gupta, aditig@andrew, Wed 4-6pm
Deepayan Patra, dpatra@andrew, Fri 6-8pm

Piazza: piazza.com/cmu/spring2021/15414/home

Gradescope: www.gradescope.com/courses/236329

Software: This course will teach students how to use the Why3 deductive verification platform. Installation instructions will be provided with the assignments that use this software.

Announcements

Welcome to Spring 2021! Be sure to check you are enrolled in Gradescope and Piazza. 1/28/2021