Die Studierenden erhalten ein profundes theoretisches und praktischesVerständnis fundamentaler Prinzipien und Konzepte in Programmanalyse,-verifikation und -transformation, das sie befähigt, darauf gegründeteVerfahren kompetent und adäqat anzuwenden und die Möglichkeiten undGrenzen insbesondere automatischer Verfahren zur Programmanalyse,-verifikation und -transformation fundiert einzuschätzen und zubeurteilen.
Die Vorlesung beschäftigt sich mit Konzepten und Prinzipiengrundlegender und fortgeschrittener Verfahren zur Analyse undVerifikation von Softwaresystemen. Im Mittelpunkt stehen dabei dieKonzepte von Korrektheit, Vollständigkeit und Optimalität in Analyse,Verifikation und Transformation. Die Vorlesung spannt dabei den Bogenvon Hoarescher Logik über Programm- und Datenflussanalyse zurTheorie abstrakter Interpretation und Modellprüfung. IllustrierendeTransformationen werden dabei besonders dem Bereich optimierender undverifizierender Übersetzung entnommen. Anhand regelmäßig gestellterÜbungsaufgaben werden die in der Vorlesung behandelten Themen anmaßgeschneiderten Aufgabenstellungen erprobt und angewendet.
Teil I: Motivation
Teil II: Analyse und Verifikation
Teil III: Transformation und Optimalität
Teil IV: Abstrakte Interpretation und Modellprüfung
Teil V: Abschluss und Ausblick
Literaturverzeichnis
Anhang
Die Vorbesprechung und daran anschließend die erste Vorlesung findenstatt am Mittwoch, den 06.03.2019, von 16:15 Uhr bis 17:45 Uhr imHörsaal EI3a, Elektrot.Institutsg., Gußhausstr. 25-29, 2. Stock.
Aufteilung der ECTS-Punkte:
Der Lehrveranstaltung sind 3.0 ECTS-Punkte zugeordnet. Dieseentsprechen einem durchschnittlichen Lernaufwand von 75Stunden. Dieser durchschnittliche Lernaufwand verteilt sich infolgender Weise auf die einzelnen Teile der Lehrveranstaltung:
Beurteilung von Beispielen und mündliche Prüfung. Die Gesamtnote setztsich je zur Hälfte aus der Übungsnote auf die Beispiele und der Notefür die mündliche Prüfung zusammen.
Grundlegende Kenntnisse in Theoretischer Informatik und Programmierungwerden vorausgesetzt. Kenntnisse im Übersetzerbau sind nützlich, etwaaus den Lehrveranstaltungen 185.A48 VU 4.0h "Übersetzerbau" oder185.A04 VU 2.0 "Optimierende Compiler", aber nicht zwingenderforderlich.
Die Vorlesung ergänzt die Lehrveranstaltungen 185.A04 "OptimierendeCompiler" und 185.A56 "Semantik von Programmiersprachen". Sieempfiehlt sich deshalb inbesondere für Studierende, die im Bereich vonProgrammiersprachen und Übersetzerbau einen besonderen Schwerpunktsetzen, eine Seminararbeit, ein Praktikum oder ihre Diplomarbeitanfertigen möchten.
