TU Wien:Formale Methoden der Informatik VO (Egly)

Aus VoWi

(Weitergeleitet von TU Wien:Formale Methoden der Informatik VU (Egly))

In der Studienplanaenderung 2006 der Technischen Universitaet Wien wurden "Theoretische Informatik 2" und "Formale Methoden der Informatik" (mit 3 ECTS) zu "Formale Methoden der Informatik" (mit 6 ECTS) zusammengelegt.

Studierende der TU, die "Theoretische Informatik 2" bereits im Bachelorstudium verwendet haben, können entweder diese Lehrveranstaltung absolvieren oder sie durch 6 ECTS Vertiefungs-LVAs ersetzen.
Studierende der TU, die "Theoretische Informatik 2" zwar im Bachelorstudium absolviert, aber nicht verwendet haben, können sich entweder "Theoretische Informatik 2" zusammen mit 1.5 ECTS einer Vertiefungs-LVA für "Formale Methoden der Informatik" anerkennen lassen, oder diese LVA absolvieren und "Theoretische Informatik 2" als Freifach nehmen.
Studierende der TU, die "Theoretische Informatik 2" nicht absolviert haben, müssen diese LVA absolvieren (außer, sie fallen unter die Übergangsbestimmungen der Masterstudien).

Fuer Details siehe bitte auch das FAQ Der Übergang vom alten auf den neuen Studienplan (2006).

Inhaltsverzeichnis

1 Daten
2 Inhalt
3 Ablauf
4 Vorkenntnisse
5 Vortrag
6 Übungen
7 Prüfung, Benotung
- 7.1 Dauer der Zeugnisausstellung
8 Zeitaufwand
9 Unterlagen
10 Tipps

[Bearbeiten] Daten

LVA-Leiter: Uwe Egly Bernhard Gramlich, Gernot Salzer Hans Tompits Prof. Pichler
ECTS: 6 (SWS: 4)
HP der LVA: http://www.logic.at/lvas/185291/
Institut: E185/2 - Institut für Computersprachen, Abteilung Theoretische Informatik und Logik
Pflichtfach für alle Masterstudien der TU Wien. (931 bis 939)

[Bearbeiten] Inhalt

Prädikatenlogik als Spezifikationssprache
Wiederholung aussagen- und prädikatenlogischer Konzepte inklusive Beweismethoden (TC0, Natural Deduction)
BDDs
Spezifikation und Verifikation von Hardware mit angewandten Logiken wie LTL und CTL
Grundlagen der formalen Programmverifikation und der formalen Programmsemantik
Modallogiken
Komplexitätstheorie: Problemreduktion, polynomielle Hierarchie, Erläuterung der wichtigsten TIME- und SPACE-Klassen

[Bearbeiten] Ablauf

Hauptsächlich Vortrag. Meist am Ende jedes Themenblocks werden Übungsblätter durchbesprochen (keine Kreuzerlübung!). Am Ende des Semesters gibt es eine Prüfung.

[Bearbeiten] Vorkenntnisse

Der Stoff des Logik-Teils von Theoretische Informatik und Logik wird als bekannt vorausgesetzt und sollte dementsprechend beherrscht werden. Es geht auch ohne, allerdings ist anfangs die Einarbeitungszeit deutlich höher.

Aussagen- und Prädikatenlogik wird aber am Beginn des Logik-Blocks von Prof. Egly wiederholt. Wer sich noch daran erinnern kann hat sicher einen gewissen Vorteil, ich denke aber dass der Aufwand auch ohne diese Kenntnisse nicht wesentlich höher ist, da Prof. Egly wie üblich sehr langsam vorträgt und seine Folien detailliert erklärt. Der Meinung meines Vorposters kann ich mich somit nicht anschließen. - Christoph R.

[Bearbeiten] Vortrag

Generell gilt für alle Vortragende, dass sie die Inhalte verständlich erklären können. Auch werden zu jedem Themenblock Übungsbeispiele durchbesprochen. Man hat die Möglichkeit, in diesem Rahmen Unklarheiten zu klären. Ist daher durchaus ein Mehrwert, zur Vorlesung zu gehen, anstatt nur die Folien durchzublättern.

[Bearbeiten] Übungen

Da diese LV seit mehreren Semestern als VO angeboten wird, ist es nicht verpflichtend, die Übungsbeispiele durchzurechnen. Sinnvoll zur Vorbereitung für die Prüfung ist es aber trotzdem.

[Bearbeiten] Prüfung, Benotung

Bei der Prüfung im WS09/10 waren alle Foliensätze erlaubt (ausgenommen alte Prüfungsangaben, selbst geschriebene Zusammenfassungen oder Übungsbeispiele und deren Lösungen). Außerdem konnte man auch das Buch mitnehmen.
Die Prüfungszeit betrug im WS09/10 2 Stunden. Wenn man die Art der Beispiele kennt, geht sich das aus, ist aber nicht extrem großzügig bemessen, IMHO.

[Bearbeiten] Dauer der Zeugnisausstellung

SS09: knapp > 1 Monat
WS09: 2 Wochen

[Bearbeiten] Zeitaufwand

Je nach Interessen, Vorkenntnissen und Begabung für Formales kann der Aufwand stark variieren. Wer alles in ausreichendem Ausmaß mitbringt und immer in der Vorlesung war, kann durchaus auch mit 2 Tagen Lernaufwand eine gute Note erreichen.

Sieht man die Theorie eher als notwendiges Übel, dann sollte man den Lernaufwand nicht unterschätzen, wie das oft passiert. Der Aufwand von 6 ECTS * 25 Stunden = 150 Stunden wird jedoch meiner Meinung nach auf keinen Fall erreicht.

Andere Meinung: Ich würde mit etwa 5 Tagen Lernaufwand rechnen zum Durcharbeiten der Übungsbeispiele und Ausarbeiten der alten Prüfungsangaben.

[Bearbeiten] Unterlagen

Michael R. A. Huth, Mark D. Ryan. Logic in Computer Science – modelling and reasoning about systems, Cambridge University Press, 2004, ISBN 0-521-54310-X paperback
Materialien
und Folien

[Bearbeiten] Tipps

Die alten Prüfungsangaben durchrechnen bereitet einen sehr gut auf die Prüfung vor. Es kommen immer sehr ähnliche oder sogar gleiche Beispiele.

Prof. Pichler hat sogar ausdrücklich gesagt, dass er sicher eines aus den 6 Beispieltypen zur Prüfung gibt, die er am Ende seines Blocks präsentiert. Das gilt jedoch nur für den Komplexitätstheorie-Teil!

Die (zumindest im SS08 und davor optionalen) Übungsbeispiele sind nützlich bei der Prüfungsvorbereitung. Beispiele bei denen Beweise zu führen sind, die in dieser Form in der VO nicht durchgenommen wurden, kann man dabei jedoch auch vernachlässigen. Sie sind für die Prüfung höchstwahrscheinlich irrelevant, wie man leicht anhand der alten Angaben sieht.

Hin und wieder ist es sinnvoll, sich vorher sinnvolle Abwandlungen bereits im Voraus zu überlegen. Beispiel: Toy Programming Language im Block: Software Verifikation. In den Übungsbeispielen sind Syntax, Semantik und die Hoare-Verifikationsregel einer WHILE-Schleife zu definieren. Wie würde das bei einer FOR-Schleife aussehen? Oder bei REPEAT?