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.

Course information

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

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.