Lectures


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


Topic 01 - Introduction to Alloy

21 Aug
Course introduction
Who am I,
Grading
Formal Methods overview
Slides
Set theory recap
Slides,
Old recorded lecture
23, 28 Aug
Introduction to Alloy
Old recorded lectures
30 Aug, 04 Sep
Alloy Constraints
Old recorded lectures
06 Sep
Academia example
Old recorded lecture

Topic 02 - Dynamic Systems

11 Sep
State Machines
Old recorded lecture
13 Oct
Laboratory: Memory Management
18, 20 Sep
Temporal operators in Alloy
25, 27 Sep
Family Model as a Transition System
02 Oct
Exam 1

Topic 03 - Constraint solving for Alloy

9 Oct
Alloy proof obligations and SAT encodings
Old recorded lecture
11 Oct
SAT solving
Old recorded lecture
16 Oct
Encoding Alloy into SAT
Old recorded lecture
18 Oct
Encoding Alloy into SMT
23 Oct
Laboratory: SAT and SMT solving (async)

Topic 04 - Specifying and verifying programs with Dafny

25, 30 Out
Introduction to Dafny
Old recorded lecture
Old recorded lecture
Old recorded lecture
01, 06 Nov
Arrays, invariants and frame conditions
Old recorded lecture
Old recorded lecture
02 Nov
No class
08, 13 Nov
OO programming and verification in Dafny
Old recorded lecture
Old recorded lecture
15 Nov
No class
20 Nov
Laboratory: OO in Dafny
22 Nov
Exam 2
27, 29 Nov
Project presentations