Vorbesprechung und Anmeldung

Die Anmeldung zur Vorlesung erfolgt in diesem Semester über die Funktionalität von TUWIS++. Anmeldungen sind ab sofort bis zum Freitag, den 20.10.2006, möglich; Abmeldungen sind möglich bis zum Dienstag, den 31.10.2006, ebenfalls über TUWIS++.

Achtung: Terminverlegung

Um eine zeitliche Überschneidung mit der LVA 185.190 "Effiziente Programme" aufzulösen, wird die Vorlesung gegenüber dem ursprünglichen Termin um 105 Minuten auf Dienstag, 17:45 Uhr s.t. bis 19:15 Uhr im GM 4 Knoller-Hörsaal verlegt. Die neue 17:45-Zeit gilt erstmals am Dienstag, den 17.10.2006.

Aktueller Hinweis

Ab dem 24.10.2006 findet die Vorlesung an folgendem neuem Ort statt: Bibliothek E185/1, Argentinierstr. 8, 4. Stock.

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. anforderungsgetriebene 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 Üersetzerbau 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
30.01.2007 12. Vorlesungsteil	Erschöpfende vs. anforderungsgetriebene 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	Letzter Vorlesungsteil
23.01.2007 11. Vorlesungsteil	Partielle Redundanz- elimination: BCM, LCM und SpCM	"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	Achtung: Abweichende Zeit am 23.01.2007: 16:00 Uhr s.t. - 17:00 Uhr!
16.01.2007 10. Vorlesungsteil	DFA-Toolkit-Sicht, Beispiele	"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.
09.01.2007 9. Vorlesungsteil	Datenflussanalyse MFP, MOP, Sicherheits-, Koinzidenztheorem	"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.
12.12.2006 8. Vorlesungsteil	Von Verifikation über Analyse zur Transformation: Optimierung, Teil 2	"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	Andere Formate nicht verfügbar.
05.12.2006 7. Vorlesungsteil	Von Verifikation über Analyse zur Transformation: Optimierung, Teil 1	"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	Andere Formate nicht verfügbar.
28.11.2006 6. Vorlesungsteil	WCET-Analyse, Nachträge zu Verbänden und CPOs, Fixpunktsatz	"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.
07.11.2006 5. Vorlesungsteil	Natürliche und denotationelle Semantik	"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.
31.10.2006 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	Aktualisiert am 07.11.2006.
24.10.2006 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	Keine.
17.10.2006 2. Vorlesungsteil	Fortführung von Vorlesungsteil 1, insbesondere induktives Beweisen		Siehe Vorlesungs- teil 1 vom 10.10.2006, erweitert und ergänzt am 17.10.2006. Veranstaltungs- hinweis Kolloquiumsvortrag, Prof. Dr. Helmut Veith, 18.10.2006, 16:00 Uhr s.t., EI 5, Gußhausstr. 25-29
10.10.2006 1. Vorlesungsteil	Die Sprache WHILE, Syntax und SO-Semantik	"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	Erweitert und ergänzt am 17.10.2006 und am 30.10.2006.
04.10.2006 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	Veranstaltungs- hinweise Antrittsvorlesung, Univ.Prof. Dr. Hannes Werthner, 09.10.2006, 17:00 Uhr s.t., EI 9, Gußhausstr. 25-29 Kolloquiumsvortrag, Dr. David F. Bacon, 06.10.2006, 10:00 Uhr c.t., EI 5, Gußhausstr. 25-29

Übung Aufgabenblatt vom	Abgabe	Verfügbare Formate	Hinweise und Bemerkungen
16.01.2007	23.01.2007	Blatt 9.pdf Blatt 9.pdf.gz	Letztes Aufgabenblatt.
10.01.2007	16.01.2007	Blatt 8.pdf Blatt 8.pdf.gz	Keine.
05.12.2006	12.12.2006	Blatt 7.pdf Blatt 7.pdf.gz	Keine.
28.11.2006	05.12.2006	Blatt 6.pdf Blatt 6.pdf.gz	Keine.
07.11.2006	28.11.2006	Blatt 5.pdf Blatt 5.pdf.gz	Keine.
31.10.2006	07.11.2006	Blatt 4.pdf Blatt 4.pdf.gz	Keine.
24.10.2006	31.10.2006	Blatt 3.pdf Blatt 3.pdf.gz	Keine.
17.10.2006	24.10.2006	Blatt 2.pdf Blatt 2.pdf.gz	Keine.
10.10.2006	17.10.2006	Blatt 1.pdf Blatt 1.pdf.gz	Keine.

Zeit und Ort

Die Vorbesprechung für das Wintersemester 2006/2007 findet am Mittwoch, den 04.10.2006, von 15:00 Uhr s.t. bis ca. 15:30 Uhr im FH HS4 statt. Die Vorlesung wird ab 10. Oktober 2006 jeden Dienstag von 16:30 Uhr bis 18:00 Uhr im GM 4 Knoller-Hörsaal am Getreidemarkt 9, 1060 Wien, stattfinden (detaillierter Lageplan) stattfinden. Ab 17.10.2006 wird der Vorlesungsbeginn auf 17:45 Uhr verschoben!

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