Logical Foundations of Program Correctness

This course is an upper-level undergraduate and graduate course about the use of mathematical proof techniques to verify the correctness of programs, algorithms and computer systems. The course will cover foundational concepts in logic, the theory of programming languages, and program verification. Students will learn about computer assisted theorem proving and will learn to use a proof assistant. Classes will be organized around problem sets and in-person lectures. In addition, students will work on a semester-long project developing a proof of correctness of a program or algorithms of their choosing.