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

In der Vorlesung verwendete Folien und Aufgabenstellungen für den Übungsteil werden während der Lehrveranstaltung wöchentlich auf dieser Seite zur Verfügung gestellt. Auch die Folien zur Vorbesprechung zu dieser Lehrveranstaltung finden Sie dort.

Übung Aufgabenblatt vom	Abgabe/Nachabgabe	Verfügbare Formate	Hinweise und Bemerkungen
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. 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 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