Schedule
| Date | Topic | Reading | Assignments |
|---|---|---|---|
| Sep 2 | Course overview | Course syllabus; slides (PDF) | — |
| Sep 7 | Labour Day — no class | — | — |
| Sep 9 | Logic refresher and SAT solving | slides (PDF); COC 1.6-1.7; DP 2.2 | — |
| Sep 14 | SMT concepts and theories | slides (PDF); COC Chapter 3, 9, 10, 29 | — |
| Sep 16 | Encoding problems as SMT | slides (PDF) | Assignment 1 released |
| Sep 21 | Hoare logic and verification conditions | slides (PDF) | — |
| Sep 23 | Loop invariants | slides (PDF) | — |
| Sep 28 | Modular Verification and Dafny | slides (PDF) Dafny Paper (UofA access required) Boogie Paper Procedures and Parameters (1971) Dafny 4.11 reference |
Assignment 1 due at 11:59 p.m. MT; Assignment 2 released |
| Sep 30 | National Day for Truth and Reconciliation — no class | — | Paper Review 1 released |
| Oct 5 | Conference travel — no class | — | — |
| Oct 7 | Conference travel — no class | — | Paper Review 1 due at 11:59 p.m. MT |
| Oct 11 | — | — | Assignment 2 due at 11:59 p.m. MT; |
| Oct 12 | Thanksgiving — no class | — | — |
| Oct 14 | Interactive theorem proving and Lean | Theorem Proving in Lean 4, selected sections | Assignment 3 released |
| Oct 19 | Inductive and recursive proofs | Course notes | — |
| Oct 21 | Program verification in Lean | Course notes | — |
| Oct 26 | Proposal Discussion | — | — |
| Oct 28 | Proposal Discussion | — | Assignment 3 due at 11:59 p.m. MT |
| Oct 30 | — | — | Project proposal due at 11:59 p.m. MT; |
| Nov 2 | Trust and proof engineering in interactive theorem provers | Course notes | Paper Review 2 released |
| Nov 4 | Automation, tactics, and proof debugging | Course notes | — |
| Nov 8 | — | — | Paper Review 2 due at 11:59 p.m. MT |
| Nov 9–13 | Reading Week — no class | — | — |
| Nov 16 | Selected topic | To be announced | |
| Nov 18 | No class meeting — project work | — | — |
| Nov 23 | Selected topic | To be announced | |
| Nov 25 | No class meeting — project work | — | — |
| Nov 30 | Selected topic | To be announced | — |
| Dec 2 | Project presentations I | — | Project presentation |
| Dec 7 | Project presentations II | — | Project presentation |
The schedule is tentative. Reading details, slides, and deadlines will be added as they are assigned.
Noting that: - “COC” refers to Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007. - “DP” refers to Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2016.