LFU:online

Die Studierenden können nach Abschluss dieses Moduls Spezifikation von Programmen verstehen, erstellen und korrigieren. Sie haben die Fertigkeit erworben, Spezifikationen formal nachzuweisen. Dabei setzen sie eine Kombination aus interaktiven und automatischen Methoden ein, um ausdrucksstarke Logiken mit effizienter Beweissuche zu kombinieren.

• Validierung und Verifikation
• partielle Korrektheit und Terminierung
• automatisierte Terminierungsanalyse
• Verwendung eines SMT-solvers
• Spezifikation von Programmeigenschaften
• Verifikation von funktionalen Programmen
• Verifikation von imperativen Programmen
• Beweistechniken: Induktion, Invarianten, Generalisierungen

Wöchentliche Übungsaufgaben, die im Proseminar von den Studierenden präsentiert und diskutiert werden

wöchentliche Übungsaufgaben

Unterlagen werden auf der Kurswebseite zur Verfügung gestellt.

Kenntnisse über funktionale Programmierung und Logik.

Im Proseminar wird deutsch gesprochen, die Übungsblätter sind jedoch in englischer Sprache verfasst.