AK der Praktischen Informatik 2
LVA 185.260, VU 2.0, 2004 W
AK der Praktischen Informatik 2: Analyse und Verifikation
(zweistündige Vorlesung mit Übung; siehe auch
TUWIS++/185.260)
Achtung: Neue Homepage-URL
Die homepage zur Vorlesung ist ab sofort unter
http://www.complang.tuwien.ac.at/knoop/ak2_ws0405.html
zu finden. Bitte passen Sie Ihre bookmarks entsprechend an! Diese
Seite wird nach dem 08.10.2004 nicht mehr aktualisiert.
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...
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.
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{\ss}hausstraße statt. 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
Wahllehrveranstaltung
für folgende
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