CMPT 477 / 777 Formal Verification - Fall 2024
| Instructor |
Yuepeng Wang |
| Time and Location |
Mon 8:30 - 10:20 am @ AQ3159
Wed 8:30 - 9:20 am @ AQ3159 |
| Instructor Email |
yuepeng@sfu.ca |
| Instructor Office Hours |
Wed 9:30 - 10:30 am or by appointment |
| TA1 |
Yang He |
| TA1 Email |
yha244@sfu.ca |
| TA1 Office Hours |
Thu 3:00 - 4:00 pm @ Zoom |
| TA2 |
Qikang Liu |
| TA2 Email |
qla116@sfu.ca |
| TA2 Office Hours |
Tue 3:00 - 4:00 pm @ ASB9810 |
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/02 |
Labor Day (No Class) |
|
| 09/04 |
Introduction |
|
| 2 |
09/09 |
Propositional Logic |
|
| 09/11 |
DPLL and SAT Solving |
H1 |
| 3 |
09/16 |
Applications of SAT |
|
| 09/18 |
Constraint Solver: Z3 |
P1 |
| 4 |
09/23 |
First-Order Logic |
|
| 09/25 |
Proof Rules of First-Order Logic |
|
| 5 |
09/30 |
National Day for Truth and Reconciliation (No Class) |
|
| 10/02 |
First-Order Theories |
H2 |
| 6 |
10/07 |
First-Order Theories & First-Order Resolution |
|
| 10/09 |
First-Order Resolution |
H3 |
| 7 |
10/14 |
Thanksgiving (No Class) |
|
| 10/15 |
Hoare Logic |
|
| 10/16 |
Hoare Logic |
|
| 8 |
10/21 |
Midterm Exam |
|
| 10/23 |
SMT Solving using Z3 |
P2 |
| 9 |
10/28 |
Verification Conditions |
|
| 10/30 |
VCs with Functions and Pointers |
H4 |
| 10 |
11/04 |
Verification Tool: Dafny |
|
| 11/06 |
Verification Tool: Dafny |
P3 |
| 11 |
11/11 |
Remembrance Day |
|
| 11/13 |
Theory of Equality |
|
| 12 |
11/18 |
Theory of Equality and Theory of Rationals |
|
| 11/20 |
Theory of Linear Arithmetics over Rationals |
|
| 13 |
11/25 |
Theory of Linear Arithmetics over Integers |
H5 |
| 11/27 |
Combining Decision Procedures |
|
| 14 |
12/02 |
Time for Final Project |
|
| 12/04 |
No class |
|
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).