Lectures

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

Topic 00 - Course introduction and overview

18 May

Course introduction: Who am I,; ERE,

Formal Methods overview: Slides,; Lecture

20 May

From tests and properties to specification: Board,; Lecture

Set theory recap: Slides,; Lecture

Topic 01 - Introduction to Alloy

25 May

Set theory recap: Slides,; Lecture

Introduction to Alloy: Lecture

27 May

Introduction to Alloy: Lecture

01 Jun

Introduction to Alloy: Lecture

08 Jun

Introduction to Forge: Lecture

10 Jun

More Alloy Modelling: Lecture

Topic 02 - Dynamic Systems

15 Jun

State Machines: Lecture

17 Jun

More on dynamic systems: Lecture

22 Jun

Ordering and Transition Systems: Lecture

24 Jun

Transition Systems and Invariants: Lecture

Q&A Homework 2: Lecture

29 Jun

More on Transition Systems and Invariants: Lecture

01 Jul

Laboratory: Memory Management

Topic 03 - Constraint solving for Alloy

06 Jul

Alloy proof obligations and SAT encodings: Lecture

08 Jul

SAT solving: Lecture

13 Jul

Encoding Alloy into SAT (part 1): Lecture

Q&A Project 1: Lecture

15 Jul

Encoding Alloy into SAT (part 2): Lecture

20 Jul

Laboratory: SAT solving

22 Jul

No class

Topic 04 - Specifying and verifying programs with Dafny

27 Jul

Introduction to Dafny: Lecture

29 Jul

Introduction to Dafny: Lecture

03 Aug

Symbolic execution and loop invariants: Lecture

05 Aug

Arrays, invariants and frame conditions: Lecture

10 Aug

More on arrays and invariants: Lecture

12 Aug

OO programming and verification in Dafny: Lecture

17 Aug

Laboratory: OO in Dafny

19 Aug

More on OO in Dafny: Lecture

24 Aug

Q&A: Lecture

26 Aug

Exam

31 Aug

Make-up exam