Schedule

Slides are posted after each lecture. Each lecture has one primary reading; read it before class. Topic order and readings may be adjusted during the term.

Week 1 · What does it mean to verify?

Lecture 1 · Verification claims, experience, and AI

• Slides: posted after the lecture
• Reading: Verifying Verified Code

Lecture 2 · A verification session in SeaHorn

• Slides: posted after the lecture
• Reading: The SeaHorn Verification Framework

Week 2 · Deductive verification with Verus

Lecture 3 · Rust contracts and inductive invariants

• Slides: posted after the lecture
• Reading: Verus: Verifying Rust Programs using Linear Ghost Types; Verus guide as reference

Lecture 4 · When a proof becomes difficult; working with an agent

• Slides: posted after the lecture
• Reading: Code-level model checking in the software development workflow at AWS

Week 3 · What happens inside an SMT query?

Lecture 5 · Programming and understanding an SMT solver

• Slides: posted after the lecture
• Reading: Programming Z3, interface material and CDCL(T)

Lecture 6 · EUF and congruence closure

• Slides: posted after the lecture
• Reading: Programming Z3, EUF section

Week 4 · Verification conditions

Lecture 7 · Simplify the program until VCGen is simple

• Slides: posted after the lecture
• Reading: Bounded Model Checking for LLVM (SeaBMC), VCGen material

Lecture 8 · Encodings, solver results, and reduction choices

• Slides: posted after the lecture
• Reading: TinyTAC/VCGen notes, posted with the slides

Week 5 · Memory and ownership

Lecture 9 · Raw memory, safety, and analysis information

• Slides: posted after the lecture
• Reading: Bounded Model Checking for LLVM (SeaBMC), memory sections

Lecture 10 · Ownership and prophecy

• Slides: posted after the lecture
• Reading: RustHorn: CHC-based Verification for Rust Programs
• Complement: Ownership in low-level intermediate representation

Week 6 · Automatic invariant discovery

Lecture 11 · Abstract interpretation as invariant discovery

• Slides: posted after the lecture
• Reading: PREVAIL: Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions
• Background: Miné, Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation, introductory portions

Lecture 12 · Understanding an inferred proof and a false alarm

• Slides: posted after the lecture
• Reading: A Flow-Sensitive Refinement Type System for Verifying eBPF Programs

Week 7 · Horn clauses and induction

Lecture 13 · CHCs as a verification interface

• Slides: posted after the lecture
• Reading: Program Verification with Constrained Horn Clauses

Lecture 14 · IC3/PDR: trying to block a bad state

• Slides: posted after the lecture
• Reading: Understanding IC3

Week 8 · Property-directed reasoning

Lecture 15 · Generalization, propagation, and convergence

• Slides: posted after the lecture
• Reading: IC3, PDR, and Friends

Lecture 16 · Spacer and the effect of the encoding

• Slides: posted after the lecture
• Reading: SMT-Based Model Checking for Recursive Programs
• Notebook: Spacer on Jupyter

Week 9 · Proof assistants with AI agents

Lecture 17 · Enough Lean to inspect a formalization

• Slides: posted after the lecture
• Reading: Theorem Proving in Lean 4, selected sections

Lecture 18 · Software models and agent-assisted proofs

• Slides: posted after the lecture
• Reading: Functional Programming in Lean, selected passages on monads

Week 10 · From Rust to functional proofs

Lecture 19 · Functional translation and backward functions

• Slides: posted after the lecture
• Reading: Aeneas: Rust Verification by Functional Translation

Lecture 20 · Verifying translated software with agents

• Slides: posted after the lecture
• Reading: Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean

Week 11 · Checking verification tools

Lecture 21 · Product programs and equivalence checking

• Slides: posted after the lecture
• Reading: Relational Verification Using Product Programs

Lecture 22 · CTAC: assessing an agent-built verifier

• Slides: posted after the lecture
• Reading: CTAC notes, posted with the slides

Week 12 · Student investigations

Project presentations.