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
Wg. Erkrankung kann die Lehrveranstaltung nicht wie geplant in derersten Märzwoche beginnen. Ihr Beginn wird auf unbestimmte Zeitverschoben und ehestmöglich an dieser Stelle bekanntgegeben.
[Ursprüngliche Planung: Vorauss. am Mittwoch, den 05.03.2014, findet von 13 Uhr s.t. bis 14 Uhr imHösaal EI4 eine gemeinsame Vorbesprechung für alle am ABProgrammiersprachen und Übersetzer im SS 2014 angebotenenLehrveranstaltungen statt.Eine spezifische Vorbesprechung für die LVA "Analyse und Verifikation"findet zusammen mit der ersten Vorlesung vorauss. am Di, den 04.03.2014, um16:30 Uhr im Hörsaal EI3a statt. ]
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 "Optimierende Compiler" 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.