TU Wien:Formale Methoden der Informatik VU (Egly)

Aus VoWi
Wechseln zu: Navigation, Suche

Daten[Bearbeiten]

Inhalt[Bearbeiten]

  • Block 1: Komplexitätstheorie
Computability, Complexity, Problem reduction, polynomial hierarchy, turing machines
  • Block 2: Satisfiability
Equality logic with uninterpreted function symbols and transformation to predicate logic, SAT solving techniques
  • Block 3: Deductive Verification of Programs
Syntax and semantics, operational semantics, axiomatic semantics, Hoare/Annotation calculus
  • Block 4: Satisfiability Model Checking
Kripke structures, time logic, simulation and bisimulation, predicate abstraction, bounded model checking

Ablauf[Bearbeiten]

Fünf bis sechs Vorlesungstermine per Block mit Übungsblättern, die freiwillig bearbeitet werden können. Die Teilnahme an Diskussionsterminen nach Ende der Übung ist ebenfalls nicht mehr verpflichtend, aber stark zu empfehlen.

Verpflichtende Vorlesungsprüfung am Semesterende zum Inhalt von allen vier Blöcken. Diese ist die einzige Grundlage zur Benotung (die Übungen werden nicht bewertet). Man bekommt nur bei einem (und für jeden) Prüfungsantritt ein Zeugnis.

Vorkenntnisse[Bearbeiten]

Der Stoff des Logik-Teils von Theoretische Informatik und Logik VU (Fermüller, Oswald) 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[Bearbeiten]

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:
Ausgenommen 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[Bearbeiten]

Modus seit WS2012: Die LVA wird zwar als VU abgehalten, die Übungsaufgaben sind aber nicht (mehr) verpflichtend und haben auch keinen Einfluss auf die Note. Es gibt zu jedem Block ein Übungsblatt mit je zehn Beispielen. Diese Beispiele sind freiwillig zu bearbeiten - es gibt vor jeder Deadline eine dedizierte Fragestunde. Wenn Beispiele abgegebenen werden, erhält man auch Feedback. Nach der Deadline gibt es einen Termin, an dem die Musterlösungen präsentiert werden. Es empfiehlt sich aber dennoch, die Übungen zu machen, weil der viele Stoff für die Prüfung sonst garantiert zuviel wird.

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

Prüfung, Benotung[Bearbeiten]

  • Zur positiven Absolvierung der LVA muss eine schriftliche Vorlesungsprüfung über alle vier Blöcke absolviert werden (der Übungsteil ist freiwillig und hat keinen Einfluss auf die Benotung). Jeder Prüfungstermin kann genutzt werden, jedoch wird für jeden Antritt ein Zeugnis ausgestellt. Der hohe Umfang des Prüfungsstoffs sollte nicht unterschätzt werden - ohne gute Vorbereitung zur Prüfung zu gehen kostet mit ziemlicher Wahrscheinlichkeit einen Versuch!
  • Auf die Prüfung können maximal 60 Punkte (= 15 Punkte pro Block) erreicht werden. Bei >= 30 hat man eine positive Note. Yay!
  • Zur Prüfung sind keine Unterlagen erlaubt (closed book). Die Prüfungszeit beträgt 2 volle Stunden. Wenn man die Art der Beispiele kennt und ein paar Prüfungen durchgerechnet hat, geht sich das aus, die 30 Minuten pro Block sind aber nicht extrem großzügig bemessen.
  • WS18 Benotung (Prfg. 16.03) - Ich bin zur Einsichtnahme gegangen obwohl ich positiv war damit ich hier meine Eindrücke teilen kann. Block 1 habe ich beide Richtungen der Reduktion zeichen können, aber irgendwie hat doch die "eigentliche" Reduktion gefehlt -4 Punkte. Block 2 hat irgendwas mit dem allquantor bei der theory of arrays with extnsionality nicht gepasst (obwohl ichs wie in den folien gemacht hab) -4 Punkte. Block 3 hab ich eine Implikation in der while Schleife mit if nicht zeigen können -3 Punkte. Block 4 - Abzüge weil die implikation nicht richtig gezeigt wurde und weil ich ein beispiel bewiesen hab obwohls falsch war :)

Dauer der Zeugnisausstellung[Bearbeiten]

  • WS14: Prüfung 08.05.2015 -> Note 01.06.2015 (24 Tage)
  • WS15: Prüfung 18.03.2016 -> Note 21.04.2016 (34 Tage)
  • WS15: Prüfung 06.05.2016 -> Note 01.06.2016 (26 Tage)
  • SS16: Prüfung 01.07.2016 -> Note 13.07.2016 (12 Tage)
  • WS16: Prüfung 21.10.2016 -> Note 21.11.2016 (31 Tage)
  • WS16: Prüfung 09.12.2016 -> Note 22.12.2016 (13 Tage)
  • WS17: Prüfung 26.01.2018 -> Note 01.03.2018 (34 Tage)
  • WS17: Prüfung 16.03.2018 -> Note 20.04.2018 (35 Tage)
  • WS17: Prüfung 04.05.2018 -> Note 11.05.2018 (7 Tage)
  • WS17: Prüfung 29.06.2018 -> Note 15.07.2018 (16 Tage)
  • SS18: Prüfung 19.10.2018 -> Note 14.11.2018 (26 Tage)
  • WS18: Prüfung 11.12.2018 -> Note 14.12.2018 (3 Tage)

Zeitaufwand[Bearbeiten]

(WS08, kontrovers) 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.

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

(WS11) Andere Meinung: Jemandem, dem der Stoff nicht liegt steckt schon mal gut und gerne 100 Stunden 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.

(SS12) Aufwandsschätzung:

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)

(WS17) Der Vorposter beschäftigt sich wohl in seiner Freizeit gern mit dem LVA Inhalt - das ist der einzige Weg wie man hier mit 2 Tagen Lernaufwand ne gute Note kriegen kann. Ansonsten ist selbst wenn man die Vorlesung besucht hat ca. 40-60h durchaus realistisch dafür (1er oder 2er, wenn man Pech hat 3er). Insgesamt fällt hier eindeutig auf dass viel zu viel Stoff in die LVA gepfercht wird, sodass ich den Gesamtaufwand auch auf ca. 8-9 ECTS schätzen würde. (Edit: der Beitrag des Vorposters wurde gelöscht)

(WS17) Already over 300h invested (wasted) into this lecture, and until the exam will throw for sure at least 50h more -> feeling no guarantee to pass the exam! In each of the math lectures and exercises had grades 2 or 3, theoretic informatic and logic (TIL) grade 1. The material of FMI is for me personally not that much uninteresting, but the way it is taught is terrible, not taking into account that this lecture had to be 4x3ECTS lecture(s) instead!

(WS18) I did the business informatics bachelor and switched then to software engineering and also I am not the best when it comes to formal methods so I did not have the best cards to start with. I watched all lecture videos and learned the complete theory behind the concepts. I found this neccessary to do the examples and not waste a lot of time searching for the why's and so (you do that anyway with certain proof steps). For the exam I learned five weeks every day with a minimum of two hours and in the end more like five or six hours a day. In the end I managed to get a "good" (2) on the exam. So I easily invested 100 hours in the exams only and in total about 150 or more.

(SS18) Ich habe mit etwas mehr als einer Woche Prüfungen rechnen, alte Ausarbeitungen durchlesen etc. ein knappes Sehr Gut geschafft. Aufwand dafür würde ich auf 8 ECTS einschätzen (auch wenn man sich mit weniger zufrieden gibt, sind die nominellen 6 ECTS eher eine untere Schranke). Was man bei den Übungsrunden nicht gemacht hat, bleibt einem bei der Prüfungsvorbereitung nicht erspart.

Unterlagen[Bearbeiten]

  • Alte Prüfungsangaben und Notenstatistiken sind auf den Institutswebsites zu finden: www.logic.at bzw. dbai.tuwien.ac.at (werden unterschiedlich oft aktualisiert)
  • Die Vortragenden stellen alle Folien, Lösungen für die Übungsblätter und zusätzliches Material im TUWEL-Kurs zur Verfügung
  • Opencast-Aufzeichnungen aller Vorträge zum Nachschauen (nicht öffentlich, man muss über TUWEL zugreifen)
  • Materialien
  • Bücher sind bei den Materialien zu finden.
    • Buch für Block1: Computational Complexity (Papadimitriou)
    • Buch für Block2: Decision Procedures An Algorithmic Point of View (Kroening)
    • Buch für Block3: The Science of Programming (Gries)
    • Buch für Block4: Model Checking (Clarke)
  • 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 (dieses Buch stellen die Vortragenden im TUWEL Kurs zur Verfügung)

Tipps[Bearbeiten]

  • (SS18) Der größte Fehler den man machen kann ist die LVA-Leitung beim Wort zu nehmen wenn sie von einem "optionalen" Übungsteil reden. Jede einzelne Aufgabe ist wichtig für das Verständnis und fast jede Aufgabenstellung kann bei der Prüfung kommen, man sollte JEDES einzelne Beispiel bei den Übungen eigenständig und vollständig durcharbeiten. Noch dazu sind 2 Stunden für die Prüfung auch nicht ewig viel Zeit - man muss schon eine gewisse Routine beim Lösen solcher Aufgaben haben, um da mit allem fertig zu werden.
  • (WS18) learn everything from each block because all the exames are so random that there are many possibilities how your exam will look like (there are seldom two times the same). Start early enough.
  • Die alten Prüfungsangaben durchrechnen bereitet einen sehr gut auf die Prüfung vor. Es kommen immer sehr ähnliche oder sogar gleiche Beispiele.
    • (WS17) Das gilt weniger für Block 2 (Satisfiability), da variieren die Fragen stark. Es ist daher zu empfehlen, bei den anderen Blöcken sattelfest zu sein.
  • Die optionalen Übungsblätter 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.
    • (WS17) Das gilt nicht mehr für Block 2 (Satisfiability). Dort kann eigentlich alles verlangt werden, was Folien und Übungsblätter so her geben.
  • 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?
  • (SS12) 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.
  • Ich kann jedem nur wärmstens empfehlen vor der Prüfung ein Buch zum Thema Logic, Theorem Proving und Verification zu lesen! Zum Beispiel: Mathematical Logic for Computer Science Third Edition von Mordechai Ben-Ari (pdf-Datei von Bibliothekswebseite), welches große Teile des LVA-Inhalts von Block 2, 3 und teilweise 4 behandelt. (Oder auch Logic in Computer Science von Michael R. A. Huth, Mark D. Ryan).

Verbesserungsvorschläge / Kritik[Bearbeiten]

  • (WS12) Den bei der Prüfung verlangten Stoff vollständig via Folien verfügbar machen!
  • (WS12) Weniger Köche mitarbeiten lassen
  • (WS12) Profs und Assis haben gegenseitig wenig Ahnung, was die andere Hand tut und man trifft auf Unverständnis sollte man mit ihrer Art zu unterrichten nicht zurande kommen (Legitimation sind allerseits die "großzügigen" 6ECTS)
  • (SS14) Streicht dieses sch**** Fach gefällgst von der Pflicht-Fach Liste, das ist sehr nett für Leute die es interessiert, aber auch ein studierter Informatiker von heute braucht es so genau nicht wissen und es ist einfach eine Frechheit, dass die formale Theorie in diesem Umfang von Informatik-Studenten verlangt wird, deren Kern-Interessen woanders liegen
  • (SS17) Eine furchtbare Lehrveranstaltung. Eigentlich sind es vier 3ECTS Lvas, welche in eine 6ECTS LVA gepfercht wurden. Auch mit solider Vorbereitung (>= 2 Monate) kann für Studierende, die sich mit der Materie schwer tun, die Prüfung ein Glücksspiel bleiben. Warum diese LVA außerdem eine VU ist, ist mir schleierhaft. Der Übungsteil ist freiwillig und trägt in keinster weise zur Note bei. Ach, und btw: der Block von Prof. Egly is der gschissenste!