Difference between revisions of "TU Wien:Formale Methoden der Informatik VU (Egly)"

From VoWi
Jump to navigation Jump to search
Similarly named LVAs (Resources):
(Egly-Bash relativiert)
m
Line 94: Line 94:
  
 
== Verbesserungsvorschläge / Kritik ==
 
== Verbesserungsvorschläge / Kritik ==
* Der folgende seit einiger Zeit epidemische Hinweis ist wohl von einem notorischen Egly-Hasser erstellt worden und geht an der Realität um Längen vorbei. Speziell in dieser LVA ist der Egly-Teil bei weitem nicht der schwierigste. Das Egly-Übungsblatt war dieses Semester (SS12) sogar das allerleichteste. Wir wurden gut vorbereitet und mit Material versorgt (u.a. Ausarbeitung des entsprechenden Blattes vom vorhergehenden Semester). Auch das Egly-Prüfungsbeispiel beim ersten SS12-Termin war mit etwas lernen absolut schaffbar und in keinster Weise unfair oder überzogen. (Dabei bin ich selbst eigentlich kein großer Fan des Egly-Stils, aber dieses Bashing ist fehl am Platz.)
+
* Der folgende seit einiger Zeit epidemische Hinweis ist wohl von einem notorischen Egly-Hasser erstellt worden und geht an der Realität um Längen vorbei. Speziell in dieser LVA ist der Egly-Teil bei weitem nicht der schwierigste. Das Egly-Übungsblatt war dieses Semester (SS12) sogar das allerleichteste. Wir wurden gut vorbereitet und mit Material versorgt (u.a. Ausarbeitung des entsprechenden Blattes vom vorhergehenden Semester). Auch das Egly-Prüfungsbeispiel beim ersten SS12-Termin war mit etwas lernen absolut schaffbar und in keinster Weise unfair oder überzogen. (Dabei bin ich selbst eigentlich kein großer Fan des Egly-Stils, aber dieses Bashing ist fehl am Platz.) -- [[Benutzer:Jabb|Jabb]] 18:58, 30. Jun. 2012 (CEST)
 
* Seit Uwe Egly 3. Stellvertreter des Studiendekans ist, sind seine LVAs auch bei Interesse am Inhalt nicht mehr studierbar und sollten nur freiwillig besucht werden, wenn man der Mathematik recht zugetan ist. Alte Prüfungsangaben/Fragenkataloge und die Bewertung des Schwierigkeitsgrades sind komplett überholt.
 
* Seit Uwe Egly 3. Stellvertreter des Studiendekans ist, sind seine LVAs auch bei Interesse am Inhalt nicht mehr studierbar und sollten nur freiwillig besucht werden, wenn man der Mathematik recht zugetan ist. Alte Prüfungsangaben/Fragenkataloge und die Bewertung des Schwierigkeitsgrades sind komplett überholt.
  

Revision as of 18:58, 30 June 2012

Achtung, die Informationen auf dieser Seite, speziell den Aufwand betreffend, sind veraltert.


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

Daten

|Master Logic and Computation |Pflichtmodul Unbekannt oder "Prä-Modul-Ära" - EDIT ME |- |Master Visual Computing |Pflichtmodul Unbekannt oder "Prä-Modul-Ära" - EDIT ME |- | E066933 |Pflichtmodul Unbekannt oder "Prä-Modul-Ära" - EDIT ME |- | E066934 |Pflichtmodul Unbekannt oder "Prä-Modul-Ära" - EDIT ME |- |Master Media and Human-Centered Computing |Pflichtmodul Unbekannt oder "Prä-Modul-Ära" - EDIT ME |- |Master Medizinische Informatik |Pflichtmodul Unbekannt oder "Prä-Modul-Ära" - EDIT ME |- |Master Software Engineering & Internet Computing |Pflichtmodul Unbekannt oder "Prä-Modul-Ära" - EDIT ME |- |Master Technische Informatik |Pflichtmodul Unbekannt oder "Prä-Modul-Ära" - EDIT ME |- | E066939 |Pflichtmodul Unbekannt oder "Prä-Modul-Ära" - EDIT ME |-


Inhalt

  • Block 1 = Komplexitätstheorie: Computability, Complexity, Problem reduction, polynomial hierarchy, turing machines
  • Block 2 = SAT solving: Equality logic with uninterpreted function symbols and transformation to predicate logic, SAT solving techniques
  • Block 3 = Formal verification of software: Syntax and semantics, operational semantics, axiomatic semantics, Hoare/Annotation calculus
  • Block 4 = Model checking: Time logics, Büchi automata, simulations and bisimulations, predicate abstractions

Ablauf

Fünf bis sechs Vorlesungstermine per Block mit verpflichtenden Übungen zu jedem Block. Teilnahme an Diskussionsterminen nach Ende der Übung verpflichtend aber kein Vorrechnen. Verpflichtende Prüfung am Semesterende.

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.

Vortrag

Generell gilt für alle Vortragende, dass sie die Inhalte verständlich erklären können. Auch werden zu jedem Themenblock die Übungsbeispiele nach den Übungsrunden 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.

Nachtrag: Besonders die Folien zu Block 3 und 4 sind eher als Unterstützung der Vorlesung denn als Lernmaterial geeignet. Vor allem die Folien zu Block 4 sind quasi unmöglich nachvollziehen ohne die Vorlesung besucht zu haben (see Predicate abstraction and CEGAR method slides)

Divergierende Meinung:
Außgenommen Pichler fand ich die Vorträge äußerst bescheiden und verkürzt, für die Stoffmenge war (zumindest WS11) viel zu wenig Zeit vorgesehen. Die Vorträge gehen dabei am Kern der Themen oft vorbei, es wird auf Details von Syntax und Semantiken stark eingegangen, wobei der Sinn und Hintergrund des Stoffes vernachlässigt wird.

Übungen

Die LVA wird (wieder) als VU abgehalten. Die verpflichtende Übung besteht aus vier Übungsblättern. Für jedes Blatt waren mindestens 2 Wochen Zeit im SS11, meist ein bisschen mehr. Es lohnt sich definitiv alle Übungsrunden zu absolvieren, auch wenn das für eine positive Bewertung nicht zwingend notwendig ist. Die Übung hilft, ein tieferes Verständnis für den Stoff zu bekommen, das grundsätzlich notwendig bei der Prüfung ist.

Viele Übungsaufgaben sind sehr zeitaufwendig, es wird aber von Seiten der Lehrenden erwartet, viel mehr Zeit zu investieren, als vorgesehen ist.

Prüfung, Benotung

  • Zur positiven Absolvierung der LVA müssen sowohl der Übungs- als auch Prüfungsteil positiv sein. Es wurde in der Vorbesprechung erwähnt, dass jeder Prüfungstermin genutzt werden kann. Jedoch wird nach jedem Versuch ein Zeugnis ausgestellt. Daher ist dieser Vorschlag eher mit Vorsicht zu genießen. Auf gut Glück zur Prüfung zu gehen kostet mit ziemlicher Wahrscheinlichkeit einen Versuch.
  • Seit WS11 ist die Prüfung closed book, es sind somit keine Unterlagen mehr erlaubt.
  • 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.

Dauer der Zeugnisausstellung

  • SS09: knapp > 1 Monat
  • WS09: 2 Wochen
  • WS11: > 1 Monat

Zeitaufwand

Aktuelle Meinung:

4 Stunden Vorlesung ~ 11 Wochen
2 8-Stunden-Tage für 5 Beispielrunden
2 40-Stunden-Wochen Prüfungsvorbereitung
-> 204h ~ 8 ECTS (6 ECTS sind vorgesehen)

((( Veraltet: 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.
  • Jemandem, dem der Stoff nicht liegt steckt schon mal gut und gerne 100Stunden in die ÜbungsausarbeitungEN (was KEINE super Note impliziert) und steckt dann noch anständig Zeit in die Prüfung. 150 Stunden sind realistisch.
  • Alleine die Ausarbeitungen der Uebungszettel nehmen schon einen Grossteil des vorgesehenen Aufwandes von 10h pro Uebungsblatt in Anspruch, wenn man wenig Erfahrung mit Graphen/... in LaTeX hat. Insgesamt werden die 150h mit dem Lernen auf die ClosedBook Pruefung leicht erreicht.

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


Man kann sich jede Menge zeit sparen wenn man Übungsbeispiele mit Graphen schön auf einen Zettel zeichnet und eingescannt ins pdf gibt,.. oder die Graphen in jedem program außer latex zeichnet.
Update SS2011 Handschriftliche Abgabeteile waren nicht mehr erwünscht

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
  • Die alten Prüfungsangaben sind auf http://www.logic.at/lvas/fminf/ zu finden

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?

Der Schwierigkeitsgrad der Prüfungen ist seit den letzten Prüfungen im SS11 angestiegen. Dementsprechend sieht auch die Notenstatistik aus. Eine äußerst solide Vorbereitung auf die Prüfung ist daher zwingend notwendig.

Bei den Übungsaufgaben hilft es, immer streng formal nach den Definitionen vorzugehen. Logisch sind die Aufgaben oft trivial, aber es soll auch formal gezeigt werden, dass die Lösung korrekt ist.

Verbesserungsvorschläge / Kritik

  • Der folgende seit einiger Zeit epidemische Hinweis ist wohl von einem notorischen Egly-Hasser erstellt worden und geht an der Realität um Längen vorbei. Speziell in dieser LVA ist der Egly-Teil bei weitem nicht der schwierigste. Das Egly-Übungsblatt war dieses Semester (SS12) sogar das allerleichteste. Wir wurden gut vorbereitet und mit Material versorgt (u.a. Ausarbeitung des entsprechenden Blattes vom vorhergehenden Semester). Auch das Egly-Prüfungsbeispiel beim ersten SS12-Termin war mit etwas lernen absolut schaffbar und in keinster Weise unfair oder überzogen. (Dabei bin ich selbst eigentlich kein großer Fan des Egly-Stils, aber dieses Bashing ist fehl am Platz.) -- Jabb 18:58, 30. Jun. 2012 (CEST)
  • Seit Uwe Egly 3. Stellvertreter des Studiendekans ist, sind seine LVAs auch bei Interesse am Inhalt nicht mehr studierbar und sollten nur freiwillig besucht werden, wenn man der Mathematik recht zugetan ist. Alte Prüfungsangaben/Fragenkataloge und die Bewertung des Schwierigkeitsgrades sind komplett überholt.