Haben Sie Interesse an einem geförderten Auslandsstudium?

Informationen zu Fördermöglichkeiten finden Sie hier.

Anmeldesystem freigeschaltet!

Das elektronische Anmeldesystem ist freigeschaltet. Sie können sich ab sofort bis zum 20. März 2009 für die Teilnahme an der Lehrveranstaltung "Analyse und Verifikation" anmelden. Bis zum 31. März 2009 können Sie sich gegebenenfalls auch wieder abmelden. Nach dem 31. März 2009 gehe ich davon aus, dass Sie die Lehrveranstaltung fest in Ihren Stundenplan aufgenommen haben und sie erfolgreich bis zum Ende besuchen wollen.

Zum Anmeldesystem.

Vorlesungstermine

Terminänderungen und -ergänzungen werden rechtzeitig an dieser Stelle bekanntgegeben.
Mi, 24.06.2009, 18:00 - 19:30 s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte)
Mi, 17.06.2009, 18:00 - 19:30 s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte)
Mi, 10.06.2009, 18:00 - 19:30 s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte)
Mi, 03.06.2009, 18:00 - 19:30 s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte)
Mi, 27.05.2009, 18:00 - 19:30 s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte)
Mi, 06.05.2009, 18:00 - 19:30 Uhr s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte)
Di, 21.04.2009, 13:30 - 15:00 Uhr s.t., FH Hörsaal 4, Freihaus, Wiedner Hauptstr. 8
Di, 17.03.2009, 13:30 - 15:00 Uhr s.t., FH Hörsaal 4, Freihaus, Wiedner Hauptstr. 8
Di, 10.03.2009, 13:30 - 15:00 Uhr s.t. FH Hörsaal 4, Freihaus, Wiedner Hauptstr. 8

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

Vorlesungsfolien

Die Vorlesungsfolien für das SS 2009 werden im Lauf des Semesters als Gesamtdokument in zwei Formaten zur Verfügung gestellt:

4 Folien pro Seite: "4 F/S".pdf und "4 F/S".pdf.gz (Stand: 23.06.2009)
8 Folien pro Seite: "8 F/S".pdf und "8 F/S".pdf.gz (Stand: 23.06.2009)
Zusatzmaterial: Constant Progagation auf dem Value Graph: "4 F/S".pdf und "4 F/S".pdf.gz (Stand: 06.06.2009)

(Die Folien werden im Lauf des Semesters bei Bedarf aktualisiert.)

Folien Vorbesprechung

Die Folien zur Vorbesprechung für das SS2009 sind in zwei Formaten verfügbar:

4 Folien pro Seite: "4 F/S".pdf und "4 F/S".pdf.gz (Stand: 10.03.2009)
8 Folien pro Seite: "4 F/S".pdf"8 F/S".pdf und "4 F/S".pdf"8 F/S".pdf.gz (Stand: 10.03.2009)
Folien der gemeinsamen Vorbesprechung (pdf) vom 04.03.2009

Übungen

Übung Aufgabenblatt vom	Abgabe	Verfügbare Formate	Hinweise und Bemerkungen
17.06.2009	24.06.2009	Blatt 8.pdf Blatt 8.pdf.gz	Keine.
10.06.2009	17.06.2009	Blatt 7.pdf Blatt 7.pdf.gz	Keine.
04.06.2009	10.06.2009	Blatt 6.pdf Blatt 6.pdf.gz	Keine.
28.05.2009	03.06.2009	Blatt 5.pdf Blatt 5.pdf.gz	Keine.
06.05.2009	27.05.2009	Blatt 4.pdf Blatt 4.pdf.gz	Keine.
06.05.2009	27.05.2009	Blatt 3.pdf Blatt 3.pdf.gz	Keine.
24.04.2009	06.05.2009	Blatt 2.pdf Blatt 2.pdf.gz	Keine.
17.03.2009	31.03.2009	Blatt 1.pdf Blatt 1.pdf.gz	Keine.

Zeit und Ort

Die Vorbesprechung (und im Anschluss daran die erste Vorlesung) für das Sommersemester 2009 finden am Dienstag, den 10.03.2009, von 13:30 Uhr bis 15:00 Uhr im FH Hörsaal 4 im Freihaus, Wiedner Hauptstr. 8, 1040 Wien, statt. Dieser Dienstagstermin und Ort ist auch der regelmäßige Vorlesungstermin und -ort.

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