Die Teilnehmer sollen anhand ausgewählter Beispiele einen Überblick über klassische und fortgeschrittene Techniken zur Programmanalyse und -verifikation und ihre Anwendungsgebiete erhalten. Dabei steht im Vordergrund, einen vertieften Einblick in die zugrundeliegenden Prinzipien und Konzepte und in die Analogien zwischen Programmanalyse und Programmverifikation zu gewinnen.Die Teilnehmer sollen anhand ausgewählter Beispiele einen Überblick über klassische und fortgeschrittene Techniken zur Programmanalyse und -verifikation und ihre Anwendungsgebiete erhalten. Dabei steht im Vordergrund, einen vertieften Einblick in die zugrundeliegenden Prinzipien und Konzepte und in die Analogien zwischen Programmanalyse und Programmverifikation zu gewinnen.
Ausgewählte Themen und Fragestellungen zur Verifikation und Analyse von Programmen, z.B. intra- und interprozedurale Programmanalyse, Analyse paralleler Programme, erschöpfende vs. anforderungsgetriebene Analyse, Konzepte wie Korrektheit, Vollständigkeit und Optimalität in Analyse, Verifikation und Optimierung.
Am Mittwoch, den 07.03.2012, findet von 13 Uhr s.t. bis 14 Uhr im Hoersaal EI4 eine gemeinsame Vorbesprechung fuer alle am AB Programmiersprachen und Uebersetzer im SS 2012 angebotenen Lehrveranstaltungen statt.
Eine spezifische Vorbesprechung fuer die LVA Analyse und Verifikation findet zusammen mit der ersten Vorlesung am Di, den 20.03.2012, um 16:30 Uhr im Hoersaal EI3a statt.
Beurteilung von Beispielen und mündliche Prüfung. Weitere Angaben zum Beurteilungs- und Prüfungsablauf finden sich auf der homepage der Lehrveranstaltung.
Die Vorlesung ergänzt die Lehrveranstaltungen 185.274 Weiterführender Übersetzerbau, 185.276 Analyse und Verifikation und 185.205 Semantik von Programmiersprachen. Sie empfiehlt sich deshalb inbesondere für Studierende, die im Bereich von Programmiersprachen und Übersetzerbau einen besonderen Schwerpunkt setzen, eine Seminararbeit, ein Praktikum oder ihre Diplomarbeit anfertigen möchten.
