• Termersetzungssysteme, Normalisierung, Konfluenz

• Getypter und ungetypter Lambda-Kalkül

• Semantik von Programmiersprachen, Anfänge der Bereichstheorie

• Datentypen, Kodatentypen, Induktion und Koinduktion, Rekursion und Korekursion

• Programmverifikation, Floyd-Hoare-Kalkül

• Reguläre Sprachen und endliche Automaten

• Beschriftete Transitionssysteme, Bisimulation und Temporallogik

Lernziele und Kompetenzen:

Fachkompetenz

Wissen

Die Studierenden geben elementare Definitionen und Fakten zu den behandelten Formalismen wieder.

Verstehen

Die Studierenden 

• erläutern Grundbegriffe der Syntax und Semantik von Formalismen und setzen diese zueinander in Bezug

• beschreiben und erklären grundlegende Algorithmen zu logischem Schließen und Normalisierung

• beschreiben wichtige Konstruktionen von Modellen, Automaten und Sprachen

Anwenden

Die Studierenden 

• verfassen formale Spezifikationen sequentieller und nebenläufiger Programme

• verifizieren einfache Programme gegenüber ihrer Spezifikation durch Anwendung der relevanten Kalküle

• setzen formale Sprachen mit entsprechenden Automaten in Beziehung

• führen einfache Beweise über Programme mittels Induktion und Koinduktion

Analysieren

Die Studierenden

• wählen für gegebene Verifikationsprobleme geeignete Formalismen aus

• erstellen einfache Meta-Analysen formaler Systeme, etwa Konfluenzprüfung von Termersetzungssystemen

  • führen einfache Meta-Beweise über Formalismen mittels Induktion und Koinduktion

Lern- bzw. Methodenkompetenz

Die Studierenden beherrschen das grundsätzliche Konzept des Beweises als hauptsächliche Methode des Erkenntnisgewinns in der theoretischen Informatik. Sie überblicken abstrakte Begriffsarchitekturen.

Sozialkompetenz

Die Studierenden lösen abstrakte Probleme in kollaborativer Gruppenarbeit.