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
Am Mittwoch, den 06.03.2012, findet von 13 Uhr s.t. bis 14 Uhr imHösaal EI4 eine gemeinsame Vorbesprechung für alle am ABProgrammiersprachen und Übersetzer im SS 2013 angebotenenLehrveranstaltungen statt.Eine spezifische Vorbesprechung für die LVA "Analyse und Verifikation"findet zusammen mit der ersten Vorlesung am Di, den 05.03.2013, um16:30 Uhr im Hörsaal EI3a statt.
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 "Optimierender Übersetzerbau", aber nicht zwingenderforderlich.
Die Vorlesung ergänzt die Lehrveranstaltungen 185.276 "Analyse undVerifikation" 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.