Analyse und Verifikation
LVA 185.276, VU 2.0, ECTS 3.0, 2009 S
MSE/W

Analyse und Verifikation

(zweistündige Vorlesung mit Übung; siehe auch TUWIS++/185.276)

Haben Sie Interesse an einem geförderten Auslandsstudium?

Informationen zu Fördermöglichkeiten finden Sie hier.

 

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)

Voraussetzungen

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

Lehrbehelfe

Während der Lehrveranstaltung werden die verwendeten Folien und Aufgabenstellungen für den Übungsteil wöchentlich an dieser Stelle zur Verfügung gestellt.

Folien vom

Thema

Verfügbare Formate (Folien pro Seite)

Hinweise und Bemerkungen

Übung   Aufgabenblatt vom

Abgabe

Verfügbare Formate

Hinweise und Bemerkungen

Zeit und Ort

Zeit, Ort der Vorlesung und der Termin für die Vorbesprechung stehen noch nicht fest. Sie werden ebenso wie Informationen zur Anmeldung rechtzeitig auf dieser Seite bekanntgegeben.

Anrechenbarkeit

Die LVA ist anrechenbar als Wahllehrveranstaltung im Masterstudium "Software Engineering & Internet Computing (MSE/W)"

Prüfungen

Die Prüfungen zur Lehrveranstaltung sind mündlich und werden voraussichtlich in der letzten Vorlesungswoche stattfinden. Andere Termine sind nach Absprache möglich.

Vortragender

Jens Knoop, Tel.: 58801-18510, E-mail: knoop@complang.tuwien.ac.at