Analyse und Verifikation
LVA 185.276, VU 2.0, ECTS 3.0
Analyse und Verifikation
(zweistündige Vorlesung mit Übung; angeboten regelmäßig
in Sommersemestern)
Haben Sie Interesse an einem geförderten
Auslandsstudium?
Informationen zu Fördermöglichkeiten finden Sie
hier.
Die LVA 185.276 Analyse und Verifikation
wird ab Studienjahr 2008/2009 jeweils im Sommersemester eines Studienjahrs
angeboten.
Aktuelle Abhaltung
Zurückliegende Abhaltungen
Weitere allgemeine Informationen
Inhalt und Ziele
Die Vorlesung beschäftigt sich mit Konzepten und Prinzipien
grundlegender und fortgeschrittener Verfahren zur Analyse und
Verifikation von Softwaresystemen. Im Mittelpunkt stehen dabei die
Konzepte von Korrektheit, Vollständigkeit und Optimalität in
Analyse, Verifikation und Transformation. Die Vorlesung erstreckt sich
dabei von Hoarescher Logik über Programm- und Datenflussanalyse
zur Theorie abstrakter Interpretation und
Modellprüfung. Illustrierende Transformationen werden dabei
besonders dem Bereich optimierender und verifizierender
Übersetzung entnommen. Anhand regelmäßig gestellter
Übungsaufgaben werden die in der Vorlesung behandelten Themen an
maßgeschneiderten Aufgabenstellungen erprobt und
angewendet. Die Studierenden erhalten in Theorie und Praxis ein
profundes Verständnis fundamentaler Prinzipien und Konzepte in
Programmanalyse, -verifikation und -transformation, das sie
befähigt, darauf gegründete Verfahren kompetent und
adäqat anzuwenden und die Möglichkeiten und Grenzen
insbesondere automatischer Verfahren zur Programmanalyse,
-verifikation und transformation fundiert einzuschätzen und
zu beurteilen.
Voraussetzungen
- Grundlegende Kenntnisse in Theoretischer Informatik und
Programmierung werden vorausgesetzt.
- Kenntnisse im Übersetzerbau sind nützlich, etwa
aus den Lehrveranstaltungen 185.A48 VU 4.0h "Übersetzerbau"
oder 185.A04 VU 2.0 "Optimierender Übersetzerbau", aber
nicht zwingend erforderlich.
Vortragender
Jens Knoop.