CS5232: Formal Specification and Design Techniques (Spring 2026)¶
Instructor: Ilya Sergey
Lectures: Wednesdays, 10:00am-12:00pm
Location: COM1-0212
Teaching Assistant: Vladimir Gladshtein
Syllabus and Grading¶
Course Materials¶
Course Textbook: The Hitchhiker’s Guide to Logical Verification (aka LoVe) by Baanen et al. Some of the lectures will be based on the materials of new work-in-progress monograph “Practical Verifications of Data structures and Algoritmms” (aka PraVDA).
Most of the lectures will be given using a white board and via live coding sessions.
Please, email me your GitHub handle (and your name) to have access to the repository containing the code for the lectures. To work on the exercises and assignments, please, create a private fork of the course repository.
Schedule¶
The timetable below is tentative and is subject to change.
Date |
Topics |
Materials |
Homework |
|
|---|---|---|---|---|
1 |
14 Jan |
No lecture: Ilya is away |
||
2 |
21 Jan |
Types, Programs, and Proofs (I) |
||
3 |
28 Jan |
Types, Programs, and Proofs (II) |
LoVe Exercises 03 |
|
4 |
4 Feb |
Functional Programming in Lean |
LoVe Exercises 05 |
|
5 |
11 Feb |
Inductive Predicates |
LoVe Exercises 06 |
|
6 |
18 Feb |
No lecture: 2nd day of CNY |
||
Reading Week |
||||
7 |
4 Mar |
Verifying Distributed Protocols in Veil |
||
8 |
11 Mar |
Reasoning about Imperative Code |
||
9 |
18 Mar |
Verifying Imperative Programs in Velvet |
||
10 |
25 Mar |
Operational Semantics |
LoVe Exercises 09 |
|
11 |
1 Apr |
Implementing Hoare Logic in Lean |
LoVe Exercises 10 |
|
12 |
8 Apr |
Logical Foundations of Mathematics |
||
13 |
15 Apr |
Project Presentations (I) |
Will take place on Zoom |
|
RW |
22 Apr |
Project Presentations (II) |
In person, location TBA |
Software Prerequisites¶
Please, make sure to install Visual Studio Code and the following extensions and tools:
You will need both cvc5 and z3 to be on your PATH to run some of the examples.
Additional Reading and Resources¶
On Lean
On Lean-based libraries discussed in the class
Velvet: a Verifier for Imperative Programs (Loom/Velvet repository)
LeanSSR: an SSReflect-Like Tactic Language for Lean (LeanSSR repository)
Lean Community Zulip
Copyright¶
Most of the basic materials for lectures are adapted, with permission, from the 2025 edition of the “Logical Verification” course developed by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Xavier Généreux, Johannes Hölzl ,and Jannis Limperg. Slides on Hoare Logic are courtesy of Cesare Tinelli (University of Iowa).