Lectures


This page gives highlights of past lectures and provides lecture notes, reading assignments, and exercises.


Topic 01 - Introduction to Alloy

14 Aug
Course introduction
Who am I,
Grading
Formal Methods overview
Slides
Set theory recap
Slides,
Old recorded lecture
12, 21 Aug
Introduction to Alloy
Old recorded lectures
25, 27 Aug
Alloy Constraints
Old recorded lectures
01 Sep
Academia example
Old recorded lecture

Topic 02 - Dynamic Systems

03 Sep
Dynamic systems: State Machines
Old recorded lecture
05, 08 Sep
Temporal operators in Alloy
15, 17 Sep
Family Model as a Transition System
22 Sep
Laboratory: Memory Management
24, 29 Sep
No class
01 Oct
Exam 1

Topic 04 - Specifying and verifying programs with Dafny

20, 22 Oct
Introduction to Dafny
Old recorded lecture
Old recorded lecture
Old recorded lecture
27, 29 Oct
No class
03, 05 Nov
Arrays, invariants and frame conditions
Old recorded lecture
Old recorded lecture
10, 12 Nov
OO programming and verification in Dafny
Old recorded lecture
Old recorded lecture
17 Nov
Dynamic Head Data Structures
19 Nov
Laboratory: OO in Dafny
24, 26 Nov, 01 Dec
Project presentations
03 Dec
Exam 2
08 Dec
No class
10 Dec
Make-up exam