Part 2 (Week 08 -- Week 14)
The slides for the second part of the course are available online:
Lectures
- Lecture 1, 05/11, Software Specification: Towards Dependable Systems
- Lecture 2, 07/11, Formal Reasoning with Hoare Logic
- Lecture 3, 12/11, Formal Reasoning with Hoare Logic (Decorated Programs + Exercises)
- Lecture 4, 14/11, Formal Reasoning with Hoare Logic (Forward/Backward Reasoning + Program Calculation)
- Lecture 5, 19/11, Mechanising Formal Verification
- Lecture 6, 21/11, Introduction to Dafny
- Lecture 7, 26/11, Introduction to Dafny (cont.)
- Lecture 8, 28/11, Dafny: Algebraic Datatypes, Lemmas and Calculations
- Lecture 9, 03/12, Structural Induction. Linking Dafny and C#
- L9.zip: Dafny code used/demonstrated in the lecture
- Lecture 10, 05/12, Classes, Class Invariants, and Dynamic Frames
- Lecture 11, 10/12, Dynamic Frames and Separation Logic
- Lecture 12, 12/12, Separation Logic (cont.)
- Lecture 13, 17/12, Revision / Consolidation
- Lecture 14, 19/12, Invited Lecture by José Fragoso
Labs
Part 1 (Week 01 -- Week 07)
See attachments below.
Attachments
