CS 410/510 TOP: Advanced Topics in Program Verification (Spring, 2024)

Credit Hours: 4/3

Course Coordinator: Yao Li

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.

Prerequisites

  • Background in elementary discrete math and logic, e.g., CS 250 Discrete Structures I, CS 251 Discrete Structures II or equivalent classes.

Either:

  • A programming language semantics course, e.g., CS410P/510 Programming Language Semantics or CS578 Programming Language Semantics or equivalent classes, or

  • Familiar with at least one theorem prover/formal verification tool, e.g., Rocq (formerly known as Coq), Agda, Isabelle, F*, Dafny, etc., or

  • A proof assistant class, e.g., CS 410/510 TOP: Proof Assistants and Program Verification or CS410/510 Theorem Proving and Program Verification

Goals

Upon the successful completion of this class…

  • I can recognize shallow embeddings, deep embeddings, and (optionally) mixed embeddings of program semantics.

  • I can define functional correctness properties for simple programs using classical programming logics such as Hoare logic, separation logic, and incorrectness logic, etc.

  • I can describe, relate, and compare classical approaches to program verification such as forward and backward simulation, Lipton’s reduction, etc.

  • I can read research papers on program verification, identify what contributions these papers make, and explain key ideas of these papers in a written literature review and in a presentation.

  • I can evaluate both the writing and the technical presentation of a research paper on program verification.

Textbooks

None.