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 12:30-1:50pm, HH B131

Instructors:

Ruben Martins

rubenm@andrew.cmu.edu

OH: Wednesdays @ 2pm GHC 7129

TAs:

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.

---

Announcements