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.

Lectures: Tue Thu 2:00-3:20pm, DH A302

Instructors:

Matt Fredrikson mfredrik@cmu

TAs:

Abby Andam	`aandam@andrew`
Leyou Jiang	`leyouj@andrew`
Yang Pan	`yangp2@andrew`
Emily Wan	`ewan2@andrew`
Immanuel Chuks-Okoh	`ichuksok@andrew`

Office Hours

Mondays @ 1pm Gates Commons Table 2 (Abby)

Tuesdays @ 4pm Gates Commons Table 6 (Emily)

Wednesdays @ 12pm Gates Commons Table 5 (Immanuel)

Thursdays @ 4pm Gates Commons Table 3 (Yang)

Fridays @ 2pm Gates Commons Table 3 (Leyou)

Saturdays @ 3pm remote (Matt): join on Zoom

For remote office hours, sign in to OHQ to join the queue, then join the Zoom meeting and wait in the waiting room until you are admitted.

Course Sites & Enrollment:

Piazza	piazza.com/cmu/fall2026/15414	Sign up at the link (no access code required)
Gradescope	Gradescope course page	Entry code: `G64XZ7`

Software: This course will teach students how to use the Why3 deductive verification platform. See the notes on installation and editing.

Office Hours Queue: We use OHQ for all office hours sessions, in person and remote. Sign in and join the 15-414 queue when you arrive.