Analyse und Verifikation
LVA 185.276, VU 2.0, ECTS 3.0
MSE/W
Analyse und Verifikation
(zweistündige Vorlesung mit Übung)
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 erstmals im Sommersemester eines Studienjahrs
angeboten.
Aktuelle Abhaltung
Zurückliegende Abhaltungen
Weitere allgemeine Informationen
Inhalt
Im Mittelpunkt der Vorlesung stehen die Konzepte von
Korrektheit,
Vollständigkeit und
Optimalität in
- Programmverifikation
Methode von Hoare (soundness,
completeness), stärkste Nachbedingungen, schwächste
Vorbedingungen,...
- Programmanalyse
Datenflussanalyse, erschöpfende
vs. anforderungsgeleitete Analyse (exhaustive vs. demand-driven
analysis), intraprozedural, interprozedural, parallel, abstrakte
Interpretation, Model-checking,...
- Programmtransformation, speziell in der Optimierung
Ziele
- Üblick über fundamentale Prinzipien und Konzepte
in Programmverifikation, -analyse und -transformation
- Herausarbeiten und Verstehen von Gemeinsamkeiten, Analogien
und Unterschieden zwischen Programmverifikation und -analyse
- Erkennen und Einschätzen der Möglichkeiten und Grenzen
insbesondere automatischer Programmanalyse (und Optimierung)
Vorkenntnisse, empfohlene Lehrveranstaltungen
Sie sollten mitbringen:
- Grundlagen in Theoretischer Informatik, grundlegende
Programmierkenntnisse
- Kenntnisse im Übersetzerbau sind hilfreich, etwa
aus der LVA 185.311 VL 3.0h Übersetzerbau (oder aus einer
vergleichbaren Veranstaltung wie etwa der LVA Übersetzerbau
185.175 LU 3.0h bzw. 185.548 VO 2.0h aus dem
bis zum 30.09.2006 gültigen Studienplan), aber
nicht zwingend erforderlich
- Abgeschlossenes Bachelor-Studium, falls Anrechnung für
Magister-Studium geplant
Die LVA ist anrechenbar als
Wahllehrveranstaltung
im Masterstudium "Software Engineering & Internet Computing (MSE/W)".
Vortragender
Jens Knoop.