CMPT 477 / 777 Formal Verification - Fall 2025
| Instructor |
Yuepeng Wang |
| Time and Location |
Wed 1:30 - 2:20 pm @ SWH10041
Fri 12:30 - 2:20 pm @ SWH10041 |
| Instructor Email |
yuepeng@sfu.ca |
| Instructor Office Hours |
Wed 2:30 - 3:30 pm @ Zoom or by appointment |
| TA1 |
Yang He |
| TA1 Email |
yha244@sfu.ca |
| TA1 Office Hours |
Fri 3:00 - 4:00 pm @ Zoom |
| TA2 |
David Deng |
| TA2 Email |
rda102@sfu.ca |
| TA2 Office Hours |
Tue 3:00 - 4:00 pm @ ASB9810 |
| TA3 |
Sara Babaee Khanehsar
|
| TA3 Email |
sba236@sfu.ca |
| TA3 Office Hours |
Mon 3:00 - 4:00 pm @ ASB9816 |
Course Description
The goal of formal verification is to prove correctness or to find mistakes in software and other systems.
This course mainly introduces deductive verification, one of the most important and popular methods for formal verification.
In this course, we will learn logic foundations, constraint solving techniques, and proof methodologies of deductive verification.
We will also learn to work with a modern constraint solver Z3 and a deductive verifier Dafny.
Grading
- Homework 30%
- Programming Assignments 25%
- Midterm Exam 20%
- Final Project 25%
All homework, programming assignments, projects, and exams must be your own work.
Reference Book
Tentative Schedule
| Week |
Date |
Topic |
Assignment |
| 1 |
09/03 |
Introduction |
|
| 09/05 |
Propositional Logic |
|
| 2 |
09/10 |
DPLL and SAT Solving |
H1 |
| 09/12 |
Applications of SAT |
|
| 3 |
09/17 |
Constraint Solver: Z3 |
P1 |
| 09/19 |
First-Order Logic |
|
| 4 |
09/24 |
Proof Rules of First-Order Logic |
|
| 09/26 |
First-Order Resolution |
H2 |
| 5 |
10/01 |
First-Order Theories |
|
| 10/03 |
First-Order Theories |
H3 |
| 6 |
10/08 |
Hoare Logic |
|
| 10/10 |
Hoare Logic |
H4 |
| 7 |
10/15 |
Review |
|
| 10/17 |
Midterm Exam |
|
| 8 |
10/22 |
SMT Solving using Z3 |
P2 |
| 10/24 |
Verification Conditions |
|
| 9 |
10/29 |
Verification Conditions |
H5 |
| 10/31 |
Verification Tool: Dafny |
|
| 10 |
11/05 |
Verification Tool: Dafny |
P3 |
| 11/07 |
Theory of Equality |
|
| 11 |
11/12 |
Theory of Linear Arithmetics over Rationals |
|
| 11/14 |
Theory of Linear Arithmetics over Rationals |
|
| 12 |
11/19 |
Theory of Linear Arithmetics over Integers |
|
| 11/21 |
Combining Decision Procedures |
H6 |
| 13 |
11/26 |
DPLL(T) Framework |
|
| 11/28 |
Time for Final Project |
|
Academic Honesty Statement
Academic honesty plays a key role in our efforts to maintain a high standard of academic excellence and integrity.
Students are advised that ALL acts of intellectual dishonesty will be handled in accordance with the SFU Academic Honesty and Student Conduct Policies (
https://www.sfu.ca/policies/gazette/student.html).