Anmeldesystem freigeschaltet!

Das elektronische Anmeldesystem ist jetzt freigeschaltet. Sie können sich ab sofort bis einschließlich zum 17. Oktober 2004 für die Teilnahme an der Lehrveranstaltung "AK der Praktischen Informatik 1: Analyse und Verifikation" anmelden. Bis zum 31. Oktober 2004 können Sie sich gegebenenfalls auch wieder abmelden. Nach dem 31. Oktober 2004 gehe ich davon aus, dass Sie die Lehrveranstaltung fest in Ihren Stundenplan aufgenommen haben und sie erfolgreich bis zum Ende besuchen wollen.
Weitere Informationen zur Gruppeneinteilung finden Sie auf den Folien zur Vorbesprechung zu dieser Vorlesung.

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. 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
02.12.2004 7. Vorlesungsteil	Fortsetzung von Vorlesungsteil 6		Keine neuen Folien
25.11.2004 6. Vorlesungsteil	Transformationen, Korrektheit, Optimalität	"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
18.11.2004 5. Vorlesungsteil	Schwächste Vorbedingungen Fixpunktsatz Übungsaufgaben	"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
11.11.2004 4. Vorlesungsteil	Denotationelle 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
04.11.2004 3. Vorlesungsteil	Mathematische Grundlagen	"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
28.10.2004 2. Vorlesungsteil	Semantikstile	"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 11.11.2004
14.10.2004 1. Vorlesungsteil	Motivation und Einführung	"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	Folien zur Information Volle Version folgt
06.10.2004 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	Veranstaltungen Vortrag, Simon Peyton Jones, einer der Väter von Haskell, 15.10.2004 IASTE Firmenmesse, 20.10.2004

Übung Aufgabenblatt vom	Abgabe	Verfügbare Formate	Hinweise und Bemerkungen
25.11.2004	02.12.2004	Blatt 5.ps Blatt 5.ps.gz	Keine
11.11.2004	18.11.2004	Blatt 4.ps Blatt 4.ps.gz	Keine
04.11.2004	11.11.2004	Blatt 3.ps Blatt 3.ps.gz	Keine
28.10.2004	04.11.2004	Blatt 2.ps Blatt 2.ps.gz	Keine
13.10.2004	28.10.2004	Blatt 1.ps Blatt 1.ps.gz	Keine

Zeit und Ort

Die Vorbesprechung für das Wintersemester 2004/2005 findet am Mittwoch, den 6. Oktober 2004, von 15:00 Uhr s.t. bis 15:30 Uhr im Hörsaal 4 im Freihaus (FH Hörsaal 4) statt. Die Vorlesungen finden danach wöchentlich donnerstags beginnend mit dem 14. Oktober in der Zeit von 16:00 Uhr c.t. bis 18:00 Uhr im EI 6 Eckert Hörsaal in der Gußhausstraße statt (detaillierter Lageplan). Eine persönliche Anmeldung zur Lehrveranstaltung ist nötig. Der Anmeldezeitraum wird nach dem aktuellen Planungsstand vom 6. Oktober bis zum 17. Oktober 2004 reichen. Gegebenenfalls nötige Änderungen werden auf dieser Seite bekannt gegeben.

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 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