Schedule
| Date | Topic | Reading | Due |
|---|---|---|---|
| Sep 2 | Course overview | Course syllabus | — |
| Sep 7 | Labour Day — no class | — | — |
| Sep 9 | Logic refresher and SAT solving | Course notes | — |
| Sep 14 | SMT: motivation and theories | Bradley and Manna, selected sections | — |
| Sep 16 | Encoding problems as SMT | Course notes | — |
| Sep 21 | Specifications and Hoare logic | Course notes | — |
| Sep 23 | Verification conditions | Course notes | — |
| Sep 28 | Loop invariants | Course notes | — |
| Sep 30 | National Day for Truth and Reconciliation — no class | — | — |
| Oct 5 | Conference travel — no class | — | — |
| Oct 7 | Conference travel — no class | — | — |
| Oct 12 | Thanksgiving — no class | — | — |
| Oct 14 | Dafny I | Dafny documentation, selected sections | — |
| Oct 19 | Dafny II | Dafny documentation, selected sections | — |
| Oct 21 | Modular verification | Course notes | — |
| Oct 26 | Proof debugging and case studies | Course notes | — |
| Oct 28 | Why interactive theorem proving? | Course notes | — |
| Nov 2 | Lean I | Theorem Proving in Lean 4, selected sections | — |
| Nov 4 | Lean II | Theorem Proving in Lean 4, selected sections | — |
| Nov 9–13 | Reading Week — no class | — | — |
| Nov 16 | Inductive and recursive proof | Course notes | — |
| Nov 18 | Program verification in Lean | Course notes | — |
| Nov 23 | Automation and tactics | Course notes | — |
| Nov 25 | Topic to be determined | To be announced | — |
| Nov 30 | Topic to be determined | 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.