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.
Die Vorbesprechung und im Anschluss daran der erste Vorlesungstermin finden am Dienstag, den 08.03.2011, von 16-18 Uhr c.t. im Hörsaal EI 3a in der Gußhausstr. 25-29 statt. Eine allgemeine Vorbesprechung zu allen vom Arbeitsbereich Programmiersprachen und Übersetzer im SS 2011 angebotenen Lehrveranstaltungen findet am Mittwoch, den 02.03.2011, von 13-14 Uhr s.t. im Hörsaal EI4 in der Gußhausstr. 25-29 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.
Im SS 2011 bietet sich besonders der parallele Besuch der Lehrveranstaltung 185.323 Verifikation von Übersetzern an, die im Rahmen einer Erasmus/LLP-Vereinbarung mit der Martin-Luther-Universität Halle-Wittenberg, Deutschland, von Prof. Dr.habil. Wolf Zimmerman in der Zeit vom 01.03.2011 bis 11.03.2011 gehalten wird.