Haben Sie Interesse an einem geförderten Auslandsstudium?

Informationen zu Fördermöglichkeiten finden Sie hier.

Anmeldesystem freigeschaltet!

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

Zum Anmeldesystem.

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

Eine perfekte Ergänzung in diesem Semester...

Parallelbesuch der LVA Optimierende Übersetzer (185.187 VU 3.0h), Dr. Markus Schordan

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
21.01.2008 11. Vorlesungsteil	CM-Spezialitäten und Interprozedurale DFA	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Siehe auch ausgeteilten Umdruck. Letzte Vorlesung.
14.01.2008 10. Vorlesungsteil	Reverse Datenfluss- analyse	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Zur Ergänzung: "1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz
10.12.2007 9. Vorlesungsteil	Sparse Code Motion	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Keine. Veranstaltungs- hinweis Kolloquium, Prof. Dr. E.-R. Olderog, 13.12.2007, 14:00 Uhr c.t., EI 5, Gußhausstr. 25-29
03.12.2007 8. Vorlesungsteil	Lazy Code Motion	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Keine.
26.11.2007 7. Vorlesungsteil	Programmrepräsentationen; von Verifikation über Analyse zu Transformation und Optimierung	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Keine.
19.11.2007 6. Vorlesungsteil	Datenflussanalyse MFP, MOP, Sicherheits-, Koinzidenztheorem, Tool-Kit-Sicht	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Veranstaltungs- hinweis Informatik-Kolloquium, Sir Tony Hoare, 27.11.2007, 17:00 Uhr s.t., EI 9, Gußhausstr. 25-29
05.11.2007 5. Vorlesungsteil	Natürliche und denotationelle Semantik, Fixpunktsatz und mathematische Grundlagen, WCET-Analyse	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Keine.
29.10.2007 4. Vorlesungsteil	Totale Korrektheit, Korrektheit vs. Vollständigkeit	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Keine.
08.&29.10.2007 3. Vorlesungsteil	Axiomatische Semantik: Beweisskizzen vs. baumartiger Beweisstil	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Besprechung wird fortgeführt am 29.10.2007.
08.10.2007 2. Vorlesungsteil	Fortführung von Vorlesungsteil 1, insbesondere SO-Semantik von WHILE und induktives Beweisen		Siehe Vorlesungs- teil 1&2 vom 01.10.2007. Veranstaltungs- hinweis WIT-Kolloquium, Gen.Dir.Brigitte Ederer, 15.10.2007, 17:00 Uhr s.t., EI 7, Gußhausstr. 25-29
01.10.2007 1. Vorlesungsteil	Die Sprache WHILE, Syntax und Semantik von Ausdrücken	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz	Besprechung wird fortgeführt am 08.10.2007.
01.10.2007 Vorbesprechung	Motivation und Organisatorisches	"1 F/S".pdf "1 F/S".pdf.gz "4 F/S".pdf "4 F/S".pdf.gz "8 F/S".pdf "8 F/S".pdf.gz

Übung Aufgabenblatt vom	Abgabe	Verfügbare Formate	Hinweise und Bemerkungen
14.01.2008	21.01.2008	Blatt 8.pdf Blatt 8.pdf.gz	Letztes Aufgabenblatt.
10.12.2007	14.01.2008	Blatt 7.pdf Blatt 7.pdf.gz	Keine.
05.12.2007	10.12.2007	Blatt 6.pdf Blatt 6.pdf.gz	Keine.
26.11.2007	03.12.2007	Blatt 5.pdf Blatt 5.pdf.gz	Keine.
19.11.2007	26.11.2007	Blatt 4.pdf Blatt 4.pdf.gz	Keine.
08.11.2007	19.11.2007	Blatt 3.pdf Blatt 3.pdf.gz	Keine.
29.10.2007	05.11.2007	Blatt 2.pdf Blatt 2.pdf.gz	Keine.
08.10.2007	29.10.2007	Blatt 1.pdf Blatt 1.pdf.gz	Keine.

Zeit und Ort

Die Vorbesprechung (und im Anschluss daran die erste Vorlesung) für das Wintersemester 2007/2008 findet am Montag, den 01.10.2007, von 16:15 Uhr bis 17:45 Uhr im Hörsaal 14 im Haupthaus am Karlsplatz 13, 1040 Wien, statt. Dieser Montagstermin und Ort ist auch der regelmäßige Vorlesungstermin und -ort. Die Anmeldung zur Vorlesung wird über ein elektronisches Anmeldesystem erfolgen. Dieses Anmeldesystem wird nach der Vorbesprechung über diese Webseite erreichbar sein. Der Anmeldezeitraum wird ausreichend lang sein und voraussichtlich bis zum Montag, den 22. Oktober 2007, dauern.

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