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 18. März 2011 für die Teilnahme an der Lehrveranstaltung "Analyse und Verifikation" anmelden. Bis zum 31. März 2011 können Sie sich gegebenenfalls auch wieder abmelden. Nach dem 31. März 2011 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

Di, 28.06.2011: 14:00 - 15:30 Uhr Uhr s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte), Abschlusstermin.
Di, 31.05.2011: 16:30 - 18:00 Uhr Uhr s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).
Invitation!
Friday, May 27, 2011: E185.1-Lectures on ""Optimal" Spilling using Integer Linear Programming" by Dr. Florian Brandner, INRIA, ENS Lyon, France.
Thursday, May 26, 2011: 4.15 p.m. - 5.45 p.m., lecture room on the ground floor of the building Argentinierstr. 8.
Invitation!
Wednesday thru Friday, May 25-27, 2011: E185.1-Lectures on "Pitfalls in System Performance Analysis" by Ass.Prof. Matthias Hauswirth, University of Lugano, Switzerland.
Invitation!
Wednesday, May 25, 2011: E185.1-Lectures on "Software: Design and Performance" by Ass.Prof. Matthias Hauswirth, University of Lugano, Switzerland.
Di, 24.05.2011, 16:30 - 18:00 Uhr Uhr s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).
Di, 17.05.2011: 16:30 - 18:00 Uhr Uhr s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).
Di, 10.05.2011, 14:30 - 16:00 Uhr Uhr s.t., Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).
Di, 12.04.2011, 16:30 - 18:00 Uhr Uhr s.t., EI 3A Hörsaal, Alte Elektrotechnik, Gußhausstr. 25-29.
Di, 22.03.2011, 16:30 - 18:00 Uhr Uhr s.t., EI 3A Hörsaal, Alte Elektrotechnik, Gußhausstr. 25-29.
Di, 15.03.2011, 16:30 - 18:00 Uhr Uhr s.t., EI 3A Hörsaal, Alte Elektrotechnik, Gußhausstr. 25-29.
Di, 08.03.2011, 16:30 - 18:00 Uhr s.t. EI 3A Hörsaal, Alte Elektrotechnik, Gußhausstr. 25-29: Vorbesprechung und erste Vorlesung.

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.

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 2011 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: 28.06.2011)
8 Folien pro Seite: "8 F/S".pdf und "8 F/S".pdf.gz (Stand: 28.06.2011)
Zusatzmaterial: Hot-Spot Optimierer: "4 F/S".pdf und "8 F/S".pdf (Stand: 06.06.2010)

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

Folien Vorbesprechung

Die Folien zur Vorbesprechung für das SS 2011 sind in zwei Formaten verfügbar.

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

Übungen

Übung Aufgabenblatt vom	Abgabe	Verfügbare Formate	Hinweise und Bemerkungen
24.05.2011	31.05.2011	Blatt 6.pdf Blatt 6.pdf.gz	Keine.
17.05.2011	24.05.2011	Blatt 5.pdf Blatt 5.pdf.gz	Keine.
10.05.2011	17.05.2011	Blatt 4.pdf Blatt 4.pdf.gz	Keine.
20.04.2011	10.05.2011	Blatt 3.pdf Blatt 3.pdf.gz	Keine.
22.03.2011	05.04.2011	Blatt 2.pdf Blatt 2.pdf.gz	Keine.
15.03.2011	22.03.2011	Blatt 1.pdf Blatt 1.pdf.gz	Keine.

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