15-414 Bug Catching: Automated Program Verification

9 units, Carnegie Mellon University

Many CS and ECE students will be developing software and hardware that must be ultra reliable at some point in their careers. Logical errors in such designs can be costly, even life threatening. There have already been a number of well publicized errors like the Intel Pentium floating point error and the Ariane 5 crash. In this course we will study tools for finding and preventing logical errors. Three types of tools will be studied: automated theorem proving, state exploration techniques like model checking and tools based on static program analysis. Although students will learn the theoretical basis for such tools, the emphasis will be on actually using them on real examples. This course can be used to satisfy the Logic & Languages requirement for the Computer Science major.

Prerequisites: 15-122 (min C) and 15-251 (min C)

Offered: Fall 2026, Fall 2025

Courseweave needs JavaScript to show sections, workloads and planning tools.