15-414 Bug Catching: Automated Program Verification

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.

Identify and formalize program correctness. In order to reason about the existence of bugs in code, and ultimately justify their absence, we need to state what it means for the code to be correct. Students will learn how to formalize correctness using logical specifications that give precise meaning to the program's intended behavior.

Understand how to write correct software from the ground up. Writing good specifications of program correctness is essential to showing that there aren't any bugs in the code, but it is also useful for writing good code from the start. Students will develop experience reasoning about correctness as they implement functionality, learning how to write code that establishes and preserves properties and invariants needed to meet a target specification.

Apply rigorous reasoning to program correctness. Program verification is the process of mathematically proving that all possible behaviors of a given program adhere to its specification. Students will learn how to use deductive reasoning and state space exploration to realize this goal, and gain experience verifying their own code against logical correctness specifications.

Learn to use automated tools to aid in verification. Formally verifying real code is challenging, but given the scale of modern software, can also be tedious and labor-intensive. A number of tools exist for automating key parts of the verification process, notably deductive verification tools and model checkers. Students will learn how to use these tools when developing correct software, and gain experience applying them to non-trivial implementations.

Understand how verification tools work. Verification tools are not perfect, and will never be able to scale universally to all software development needs. Understanding the principles and techniques that these tools use is necessary for evaluating when it is appropriate to use a particular tool, and for addressing a tool's limitations when they arise in practice.

There is no textbook for this class, and detailed lecture notes will be posted to the website within a few days after each class. Keep in mind that lecture notes may not contain everything we cover in class. Comments and corrections are welcome, please give them to the course staff on Piazza.