LFU:online

Die Studierenden können nach Abschluss dieses Moduls Spezifikation von Programmen verstehen, erstellen und korrigieren. Sie haben die Fertigkeit erworben, Spezifikationen for-mal 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

Vortrag, Beurteilung aufgrund eines einzigen Prüfungsaktes am Ende der Lehrveranstaltung.

Schriftliche Prüfung am Ende des Semesters.

Unterlagen werden auf der Kurswebseite zur Verfügung gestellt.

Kenntnisse über funktionale Programmierung und Logik.

Die Vorlesungssprache ist deutsch, die Unterlagen sind jedoch in englischer Sprache verfasst.