CS 410/510 TOP: Proof Assistants and Program Verification

Course Description

Program testing can be used to show the presence of bugs, but never to show their absence!

—Edsger W. Dijkstra

This course will be a hands-on introduction to an interactive theorem prover called the Coq proof assistant. A proof assistant doesn’t prove things itself; rather, it helps a human construct a proof more easily and reliably in an interactive manner. If you like solving puzzles, using a proof assistant is fun and can be addictive!

We will begin by learning how to use the Coq proof assistant to mechanically reason about properties, and then progress to proofs about a program’s correctness, i.e., the absence of bugs!

The past decade has seen enormous advances in the verification of important software infrastructure, including realistic cryptographic libraries, data structure libraries, compilers, operating systems, and file systems. This is a good opportunity for you to learn more about these cutting-edge techniques.