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: Certification | pdf (x4) | |
| Part 8: Summary and Outlook | pdf (x4) |
Evaluation
Eine alte Klausur wird am 19. Juni zu Übungs-Zwecken in der Vorlesung besprochen. Die Lösung ist in OLAT zu finden.
Die 1. Klausur findet am 26. Juni statt (closed book). Eine 2. und 3. Klausur wird auf Nachfrage angeboten.