Please note:

To view the current Academic Calendar, go to

Introduction to Formal Verification CMPT 477 (3)

Introduces, at an accessible level, a formal framework for symbolic model checking, one of the most important verification methods. The techniques are illustrated with examples of verification of reactive systems and communication protocols. Students learn to work with a model checking tool. Prerequisite: CMPT 275 or 276, with a minimum grade of C-.

Section Instructor Day/Time Location
D100 Yuepeng Wang
Sep 6 – Oct 6, 2023: Tue, 12:30–2:20 p.m.
Oct 11 – Dec 5, 2023: Tue, 12:30–2:20 p.m.
Sep 6 – Dec 5, 2023: Fri, 12:30–1:20 p.m.