CS 410/510 TOP: Advanced Topics in Program Verification

Course Description

Despite decades of advancement in software development, software bugs are still a common phenomenon. In fact, it is becoming increasingly challenging to identify and fix bugs these days, with new modern technologies such as distributed systems, microservices, and LLM-assisted programming. What can we do about this?

Formal verification is a methodology of using formal logic to establish a proof that shows a program is absent 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. In this course, we will discuss both classical and new, cutting-edge approaches in program verification. We will also prepare you to understand research papers in the field of program verification.