Folien
Die Folien werden im Laufe des Semesters verfügbar gemacht.
- 1. Einführung (4 auf 1)
- 2. Eine Logik für Programm-Spezifikationen (4 auf 1) There has been a minor update of the type-checking algorithm on March 17. It now uses "return" instead of "Just" to emphasize that the proven properties do not depend on the chosen error-monad.
- 3. Semantik von Funktionalen Programmen (4 auf 1)
-
4. Überprüfung der Wohl-Definiertheit von Funktionalen Programmen
(4 auf 1)
updated version of slides (proof of Ramsey's theorem uses induction for "arbitrary c and X")
SMT2-file to search a polynomial interpretation using Z3 -
5. Verifikation von Eigenschaften Funktionaler Programme
(4 auf 1)
-
6. Verifikation von Imperativen Programmen
(4 auf 1)
-
7. Zusammenfassung und Ausblick
(4 auf 1)