Axiomatic characterization

Lecture slides

pdf git v1.11.1

Lecture videos

playlist 1h20m15s

introduction yt up
completion yt up
tightness yt up
loops yt up
summary yt up

Blue board videos

external support and loop formulas yt up

Extra slides

blue board, external support and loop formulas pdf

Errata

The slides underlying the video on loops have a bug on page 245: the theorem misses that set X must be a model of the program. This is fixed in the new version of the slides but not (yet) in the video.

Exercise sheets