Zielgruppe
Studierende des Masterstudiengangs Informatik
Form
Vorlesung (2 SWS) und Praktikum (2 SWS)
Inhalte
- Floyd Logic and Hoare Triples
- Strongest Postcondition and Weakest Precondition
- Weakest Liberal Precondition
- Lemmas and Proofs
- Functional Programs
- Imperative Program
- Dynamic Heap Data Structures
Praktikum: Programmverifikation mit Dafny
Literatur
- Buch: K. Leino, Program Proofs