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 | slides (PDF) Philip Wadler, Propositions as Types Theorem Proving in Lean 4: Dependent Type Theory, Propositions and Proofs, Tactics, and Quantifiers and Equality |
— |
| Oct 19 | Inductive and recursive proofs | slides (PDF) | Assignment 3 released |
| Oct 21 | Program verification in Lean | slides (PDF); demo |
— |
| Oct 26 | Program verification in Lean II; Proposal Discussion | slides
(PDF); demo |
— |
| Oct 28 | No class — 30-minute group project meetings in office, 12:30–4:30 p.m. MT | Book a 30-minute meeting | |
| Oct 30 | — | — | One-page project proposal due at 11:59 p.m. MT; |
| Nov 2 | Symbolic model checking | slides (PDF); Symbolic Model Checking with BDDs; Symbolic Model Checking: 10^20 States and Beyond; Interpolation and SAT-based Model Checking |
Assignment 3 due at 11:59 p.m. MT; |
| Nov 4 | No class meeting — project work | Course notes | — |
| Nov 9–13 | Reading Week — no class | — | — |
| Nov 16 | Constrained horn clauses | Course notes | Paper Review 2 released |
| Nov 18 | No class meeting — project work | — | — |
| Nov 22 | — | Paper Review 2 due at 11:59 p.m. MT | |
| Nov 23 | Memory safety I | Course notes | |
| Nov 25 | No class meeting — project work | — | — |
| Nov 30 | Memory safety II | Course notes | — |
| Dec 2 | No class meeting — project work | — | — |
| Dec 4 | — | Project Project due at 11:59 p.m. MT | |
| Dec 7 | Project presentations | — | 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.