Lectures
This page gives highlights of past lectures and provides lecture notes, reading assignments, and exercises.
Topic 00 - Course introduction and overview
- 24 Aug
- Course introduction
- Who am I,
- Grading
- Formal Methods overview
- Slides
- 29 Aug
- From tests and properties to specification
- Board from old class,
- Old recorded lecture
- 29 Aug
- Set theory recap
- Slides,
- Old recorded lecture
Topic 01 - Introduction to Alloy
- 31 Aug
- 05 Sep
- Introduction to Alloy (via Zoom)
- Recording (password: .MDc%LC8)
- Old recorded lectures
- 14 Sep
- 19 Sep
Topic 02 - Dynamic Systems
- 21 Sep
- 26, 28 Sep
- Temporal operators in Alloy
- 01 Oct
- Laboratory: Memory Management
- 03, 05 Oct
- Family Model as a Transition System
- 10 Oct
- Exam 1
Topic 03 - Constraint solving for Alloy
- 17 Oct
- 19 Oct
- 24, 26 Oct
- 26, 31 Oct
- Encoding Alloy into SMT
- 07 Nov
- No class
Topic 04 - Specifying and verifying programs with Dafny
- 09, 14 Nov
- 16 Nov
- 21, 23 Nov
- 28 Nov
- Laboratory: OO in Dafny
- 30 Nov
- Advanced Dafny features
- 05 Nov
- Exam 2
- 07 Nov
- Make-up exam