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:

• Propositional and first-order logic
• Formal proof
• Specifications of correct program behavior
• Program semantics
• Deductive program verification
• Decision procedures used in verification tools
• Fully-automated model checking
• Program abstraction techniques used in verification

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

• Office Hours: Fridays 11am (Fredrikson, CIC 2126), Thursdays 4pm (Platzer, GHC 9103)
• Email: mfredrik@cs, aplatzer@cs

TAs: Jonathan Laurent, Tianyu Li

• Office Hours: Tuesdays 2pm (Laurent, GHC 9115), Wednesdays 4:45pm (Li, GHC 6002)
• Email: jonathan.laurent@cs, tli2@andrew

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

---

Announcements