Vorbesprechung und Anmeldung

Siehe Zeit und Ort.

Das Anmeldesystem ist freigeschaltet! Zum Anmeldesystem.

Vorschau auf den abschließenden Vorlesungstermin

Mo, 23.01.2006, 16:15-17:45 Uhr, im Eckert-Hörsaal

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 Übersetzerbau (185.175 LU 3.0h bzw. 185.548 VO 2.0h), aber nicht zwingend erforderlich
Abgeschlossenes Bakkalaureat, falls Anrechnung für Magisterstudium geplant

Eine perfekte Ergänzung in diesem Semester...

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

Weiters bietet sich die Vorlesung insbesondere für Teilnehmer der Lehrveranstaltungen 185.548 VO Übersetzerbau und 185.175 LU Übersetzerbau zur Vertiefung an. Eine vorausgegangene (oder gleichzeitige) Teilnahme an diesen Veranstaltungen ist hilfreich, aber nicht Voraussetzung.

Lehrbehelfe

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

Folien vom	Thema	Verfügbare Formate (Folien pro Seite)	Hinweise und Bemerkungen
23.01.2006 10. Vorlesungsteil	Fortgeschrittene interprozedurale Datenflussanalyse		Vorlesungsunterlagen: Teil 3 des ausgeteilten Umdrucks.
16.01.2006 9. Vorlesungsteil	Reverse und interprozedurale Datenflussanalyse		Vorlesungsunterlagen: Teil 2 des ausgeteilten Umdrucks.
09.01.2006 8. Vorlesungsteil	Datenflussanalyse, Sicherheits-, Koinzidenzsatz		Vorlesungsunterlagen: Teil 1 des ausgeteilten Umdrucks.
12.12.2005 7. Vorlesungsteil	Ergänzungen: Relationen, Verbände, CPOs, stetige Funktionen und Fixpunktsätze	"1 F/S".ps "1 F/S".ps.gz "4 F/S".ps "4 F/S".ps.gz "8 F/S".ps "8 F/S".ps.gz	Keine.
28.11.2005 6. Vorlesungsteil	Von Verifikation über Analyse zur Transformation: Optimierung, Teil 2	"1 F/S".ps "1 F/S".ps.gz "4 F/S".ps "4 F/S".ps.gz "8 F/S".ps "8 F/S".ps.gz	Keine.
21.11.2005 5. Vorlesungsteil	Von Verifikation über Analyse zur Transformation: Optimierung, Teil 1	"1 F/S".ps "1 F/S".ps.gz "4 F/S".ps "4 F/S".ps.gz "8 F/S".ps "8 F/S".ps.gz	Keine.
14.11.2004 4. Vorlesungsteil	Totale Korrektheit, Korrektheit vs. Vollständigkeit	"1 F/S".ps "1 F/S".ps.gz "4 F/S".ps "4 F/S".ps.gz "8 F/S".ps "8 F/S".ps.gz	Aktualisiert am 21.11.2005.
31.10.2005 3. Vorlesungsteil	Axiomatische Semantik: Beweisskizzen vs. baumartiger Beweisstil	"1 F/S".ps "1 F/S".ps.gz "4 F/S".ps "4 F/S".ps.gz "8 F/S".ps "8 F/S".ps.gz	Aktualisiert am 02.11.2005.
24.10.2005 2. Vorlesungsteil	Semantikstile: Operationell, denotationell, axiomatisch	"1 F/S".ps "1 F/S".ps.gz "4 F/S".ps "4 F/S".ps.gz "8 F/S".ps "8 F/S".ps.gz	Aktualisiert am 14.11.2005. Aktualisiert am 02.11.2005.
17.10.2005 1. Vorlesungsteil	Die Sprache WHILE, Syntax und SO-Semantik	"1 F/S".ps "1 F/S".ps.gz "4 F/S".ps "4 F/S".ps.gz "8 F/S".ps "8 F/S".ps.gz	Aktualisiert am 02.11.2005.
10.10.2005 Vorbesprechung	Motivation und Organisatorisches	"1 F/S".ps "1 F/S".ps.gz "4 F/S".ps "4 F/S".ps.gz "8 F/S".ps "8 F/S".ps.gz	Aktualisiert am 02.11.2005. Aktualisiert am 31.10.2005. Veranstaltungs- hinweis Antrittsvorlesungen, Univ.Prof. Dr. Schahram Dustdar, Univ.-Prof. Dr. Peter Pichler, 17.10.2005, 17:00 Uhr s.t.

Übung Aufgabenblatt vom	Abgabe	Verfügbare Formate	Hinweise und Bemerkungen
12.12.2005	09.01.2006	Blatt 6.pdf Blatt 6.pdf.gz	Gemeinsam für AKdPI 1 und AKdPI 2
28.11.2005	12.12.2005	Blatt 5.pdf Blatt 5.pdf.gz	Gemeinsam für AKdPI 1 und AKdPI 2
21.11.2005	28.11.2005	Blatt 4.ps Blatt 4.ps.gz	Gemeinsam für AKdPI 1 und AKdPI 2
14.11.2005	21.11.2005	Blatt 3.ps Blatt 3.ps.gz	Gemeinsam für AKdPI 1 und AKdPI 2
02.11.2005	14.11.2005	Blatt 2.ps Blatt 2.ps.gz	Gemeinsam für AKdPI 1 und AKdPI 2
25.10.2005	31.10.2005	Blatt 1.ps Blatt 1.ps.gz	Gemeinsam für AKdPI 1 und AKdPI 2

Zeit und Ort

Die Vorbesprechung für das Wintersemester 2005/2006 wird am Montag, den 10.10.2005, von 16:15 Uhr bis 16:45 Uhr im EI 6 Eckert Hörsaal in der Gußhausstraße stattfinden (detaillierter Lageplan). Die Vorlesungen finden danach wöchentlich montags von 16:00 Uhr c.t. bis 18:00 Uhr beginnend mit dem 17.10.2006 ebenfalls im EI 6 Eckert Hörsaal statt. 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 Freitag, den 21. Oktober 2005, dauern.

Anrechenbarkeit

Die LVA ist anrechenbar als Wahllehrveranstaltung für folgende Bakkalaureatsstudien:

Data Engineering & Statistics (BDS/W)
Software & Information Engineering im Schwerpunkt "Software Engineering" (BSIa/W)
Medizinische Informatik (BZI/W)

Die LVA ist anrechenbar als Wahllehrveranstaltung für folgendes Magisterstudium:

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