Slides
The slides will be made avaiable during the semester.
| topics | slides | sources |
|---|---|---|
| Part 1: Introduction | pdf (x4) | |
| Part 2: A Logic for Program Specifications | pdf (x4) | |
| Part 3: Semantics of Functional Programs | pdf (x4) | Demo.thy |
| Part 4: Checking Well-Definedness of Functional Programs | pdf (x4) | |
| Part 5: Reasoning about Functional Programs | pdf (x4) | Demo.thy |
| Part 6: Verification of Imperative Programs | pdf (x4) | Demo.thy |
| Part 7: Summary and Outlook |