LFU:online

Absolvent:innen dieses Moduls sind in der Lage, die Semantik einer einfachen funktionalen oder imperativen Sprache formal zu spezifizieren und Techniken für Verifikation wie Hoare-Kalkül oder abstrakte Interpretation für diese zu instantiieren und anzuwenden. Sie können erklären, was die Korrektheit eines Compilers formal bedeutet.

Außerdem haben sie grundlegende Kenntnisse mit dem Beweisassistenten Isabelle/HOL erworben und sind in der Lage, einfachere mathematische Beweise selbstständig zu formalisieren.

Arten formaler Semantiken für Programmiersprachen: big-step, small-step, denotational; einfache Typsysteme; einfache Programmanalyse und -modifikation (Initialisierungsanalyse, constant folding, liveness); weakest precondition reasoning und Hoare-Kalkül; partielle und totale Korrektheit; abstract interpretation

Grundlegende Kenntnisse mit Isabelle/HOL: nichtrekursive Definitionen, rekursive Definitionen, induktive Prädikate; die strukturierte Beweissprache Isar; verschiedene Induktions- und Fallunterscheidungsschemata

Folien, ggf. ergänzt durch Tafelanschrieb. Frei verfügbares Lehrbuch. Hausaufgaben und Übungsaufgaben in Präsenz.

Schriftlich

Concrete Semantics, T. Nipkow und G. Klein, 2024.

ISBN: 978-3-319-10541-3

Frei verfügbar unter: http://www.concrete-semantics.org

Gute grundlegende Kenntnisse in Logik (Aussagenlogik, Prädikatenlogik), funktionaler Programmierung und diskreter Mathematik wie vermittelt z.B. in den Vorlesungen "Einführung in die Theoretische Informatik", "Einführung in die funktionale Programmierung", "Diskrete Strukturen", und "Logik".

Kenntnisse von Isabelle/HOL oder von Programmverifikation (z.B. Hoare-Kalkül) sind nicht notwendig, können aber hilfreich sein.

Verfahren zur Vergabe der Plätze bei Lehrveranstaltungen mit Teilnahmebeschränkung (PS, SE, VU, PJ)

Bei Lehrveranstaltungen mit einer beschränkten Zahl von Teilnehmerinnen und Teilnehmern werden die Plätze wie folgt vergeben:

1. Studierende, denen aufgrund der Zurückstellung eine Verlängerung der Studienzeit erwächst, sind bevorzugt zuzulassen.

2. Reicht Z 1 zur Regelung der Zulassung zu einer Lehrveranstaltung nicht aus, so sind an erster Stelle Studierende, für die diese Lehrveranstaltung Teil eines Pflichtmoduls ist, und an zweiter Stelle Studierende, für die diese Lehrveranstaltung Teil eines Wahlmoduls ist, bevorzugt zuzulassen.

3. Reichen Z 1 und 2 zur Regelung der Zulassung zu einer Lehrveranstaltung nicht aus, so werden die vorhandenen Plätze verlost.

Curriculum MA Informatik 2021W