Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage (u.a.)
diese Konzepte auf Methoden zur Programmtransformation/optimierung zu übertragen und anzuwenden.
Gemeinsamkeiten, Analogien und Unterschiede zwischen Programmanalyse und Programmverifikation zu verstehen und herauszuarbeiten.
die Möglichkeiten und Grenzen insbesondere automatischer und semi-automatischer Verfahren zur Programmanalyse, Programmverifikation und Programmtransformation/-optimierung im Spannungsfeld von Entscheidbarkeit, Skalierbarkeit, Wirksamkeit und Nützlichkeit zu erkennen, einzuschätzen und zu bewerten.
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
Ausgewählte Leseempfehlungen
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 Lernaktivitäten der Lehrveranstaltung(die Angaben Teil I bis Teil V beziehen sich auf die entsprechenden Teileder Lehrveranstaltungsunterlagen):
Die Lehrveranstaltung beginnt mit Vorbesprechung und erster Vorlesung am Mittwoch, den 04.03.2020, von 16:15 Uhr bis 17:45 Uhr imHörsaal EI3a, Elektrot.Institutsg., Gußhausstr. 25-29, 2. Stock.
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.