CMPUT 664: Formal Verification
Topics in Software Engineering · Fall 2026 · University of Alberta
Formal verification aims to establish mathematically rigorous guarantees about software and hardware. This course introduces the foundations and practice of modern formal verification, including automated reasoning, SMT, deductive program verification, and interactive theorem proving.
Announcements
Sep 9: The Final Project Guide is now available. It describes the expected project scope, team requirements, proposal, presentation, final report, and assessment criteria. The project proposal is due on October 30 at 11:59 p.m. MT. Please read the guide and begin discussing possible topics and teams early.
Sep 9: The course schedule has been revised. Core lecture material and the three programming assignments are now concentrated in September and October, and the final-project proposal is due on October 30. Beginning in November, we will meet once per week for selected topics; the remaining class periods are left free for independent project work. This change is intended to give project teams longer, less fragmented periods for technical work, collaboration, and presentation preparation. Please review the updated schedule for assignment deadlines and no-class dates.
Sep 3: Please submit your Github ID through here. Otherwise you will not be able to submit assignment/reviews.
Course information
| Course | CMPUT 664-A1 (58947) |
| Instructor | Jocelyn Qiaochu Chen |
| Lectures | Monday and Wednesday, 12:30–1:50 p.m. |
| Location | Education Centre 2-135 |
| Office hours | Wednesday, 4:00–5:00 p.m., UCOMM 6-230 |
| Campuswire | Course portal — (code: 5864) |
| Format | In person; lectures are not recorded |
Course goals
Students will study the logical foundations underlying modern verification tools, gain experience with SMT solvers and program verifiers, and construct machine-checked proofs in an interactive proof assistant. We will examine what different verification paradigms can establish, where their limitations lie, and how they complement one another.
The course emphasizes practical verification using tools such as Z3, Dafny, and Lean.
Prerequisites
Students should have a solid background in algorithms and data structures, proficiency in at least one programming language, and familiarity with discrete mathematics and proof techniques. Prior exposure to logic or formal methods is helpful but not required.
Assessment
| Component | Weight |
|---|---|
| Three programming labs | 45% |
| Two paper reviews | 10% |
| Final project | 45% |
See Assignments for release information and Policies for collaboration, late-work, and tool-use policies.
Communication
Official course announcements will be posted through the course Campuswire, which will open for joining at the start of the semester. The Campuswire forum is primarily for peer help: students are encouraged to ask and answer questions about lectures, assignments, and projects. The instructor will read and participate when time permits, but an instructor response to every forum post is not guaranteed.
For personal circumstances or private academic matters, send the instructor a direct message on Campuswire rather than posting in the forum or sending email. Submission instructions will appear on each assignment page when that assignment is released.
Acknowledgements
This course draws on ideas and materials from Işıl Dillig’s CS 389L, Automated Logical Reasoning, at the University of Texas at Austin, as well as ideas from Yuepeng Wang’s CMPT 477/777: Formal Verification at Simon Fraser University. Some assignment design and assessment practices are adapted from Ben Liblit’s CS 706, Analysis of Software Artifacts, at the University of Wisconsin–Madison, which I took as an undergraduate. I am grateful to all three instructors for their influence on this course.
Disclaimer
Any typographical errors in this wesbite are subject to change and will be announced in class and/or updated on the course website.