TU Wien:Formale Methoden der Informatik VU (Egly)

From VoWi
Jump to navigation Jump to search
Similarly named LVAs (Resources):

Daten[edit]

Lecturers Uwe Egly; Pamina Georgiou; Laura Kovacs; Matthias König; Sarah Sophie Sallinger; Miroslav Stankovic; Friedrich Weber; Stefan Woltran; Florian Zuleger
ECTS 6
Alias Formal Methods in Computer Science (en)
replaces Theoretische Informatik 2 VU (Baaz)
Department Logic and Computation
When winter semester
Last iteration 2021WS
Language "if required in english" was not recognized as a supported language code.
Abbreviation FMI
Mattermost formale-methoden-der-informatikRegisterMattermost-Infos
Links tiss:185291, Homepage
Zuordnungen
Master Logic and Computation Pflichtmodul Formal Methods in Computer Science
Master Software Engineering & Internet Computing Pflichtmodul Formal Methods in Computer Science
Master Technische Informatik Pflichtmodul Formal Methods in Computer Science


Inhalt[edit]

  • 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[edit]

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. Pro Semester werden üblicherweise 3 Prüfungstermine angeboten, d.h. insgesamt gibt es 6 mögliche Termine pro Studienjahr.

Vorkenntnisse[edit]

Es gibt keine formalen Voraussetzungen, allerdings gibt es gewisse Überschneidungen zu bzw. Anknüpfungen an Theoretische Informatik und Logik VU (Fermüller, Oswald). Es geht auch ohne, allerdings ist anfangs die Einarbeitungszeit deutlich höher.

Vortrag[edit]

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.

Übungen[edit]

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 (vor allem die des 2. Blocks).

Prüfung, Benotung[edit]

  • 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.
  • 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 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 zeigen 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 extensionality 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 :)
  • WS20 Regardless how we all feel about the content and difficulty of the LVA the online exam experience was amazing. At each sub-exercise you could choose between entering your solution or tuwel or write it up in any way you'd like. Whether it is typing it in latex, handwritting or tablet. Their method of supervision was also very unintrusive. They just wanted to see our faces and we all stayed mute during the exam (So no annoying background noises!). Combine this with the fact that you can write your exam in a relaxed homely environment it made for an amazing experience where I truly felt like I didn't lose points or performed worse due to stress and the general hectic exam environment in a lecture hall. As a trade off they do suspect-test people more aggressively where they might ask you to stay at the end of the exam, or on a latter date, for a small oral examination which is, at least in my opinion, incredibly fair.

Dauer der Zeugnisausstellung[edit]

Semester Prüfung Zeugnis
WS14 08.05.2015 01.06.2015 24 Tage
WS15 18.03.2016 21.04.2016 34 Tage
WS15 06.05.2016 01.06.2016 26 Tage
SS16 01.07.2016 13.07.2016 12 Tage
WS16 21.10.2016 21.11.2016 31 Tage
WS16 09.12.2016 22.12.2016 13 Tage
WS17 26.01.2018 01.03.2018 34 Tage
WS17 16.03.2018 20.04.2018 35 Tage
WS17 04.05.2018 11.05.2018 7 Tage
WS17 29.06.2018 15.07.2018 16 Tage
SS18 19.10.2018 14.11.2018 26 Tage
WS18 11.12.2018 14.12.2018 3 Tage
SS19 18.10.2019 04.11.2019 17 Tage
SS20 09.06.2020 19.06.2020 10 Tage
SS20 24.07.2020 14.08.2020 21 Tage
WS20 16.10.2020 30.10.2020 14 Tage
WS20 09.12.2020 21.12.2020 12 Tage
WS20 16.04.2021 30.04.2021 14 Tage

Zeitaufwand[edit]

(WS11) 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 Übungszettel nehmen schon einen Großteil des vorgesehenen Aufwandes von 10h pro Übungsblatt in Anspruch, wenn man wenig Erfahrung mit Graphen/... in LaTeX hat. Insgesamt werden die 150h mit dem Lernen auf die Closed Book Prüfung leicht erreicht.

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

(SS20) Circa 2 Monaten unregelmässig gelernt. Dann 2 Wochen Urlaub von der Arbeit genommen und jeden Tag min 4 Stunden in der Bib gelernt. Mit 4 bestanden. Das schwierigste Fach, das auch am meisten Zeitaufwand hat!!

(SS20) I also studied like 2,5 month for it (~2 hours a day), in the last two weeks the whole day. Start studying early enough, especially if the topics are not that easy going for you.

(SS20) I studied 4 weeks (1 week per block) intensely and then 2 more weeks were I repeated the most important exercises of the last 10 exams. I never attended any lecture, I never opened any exercise sheet. My only preparation were old exams and some slides which seemed to be important. Totally I spent maybe a bit more than 150 hours, but I had no real special interest in the topic and I am also NOT doing any of that stuff in my freetime or at work, it was completly new to me. The stuff I learnt at EWBS and TIL was long gone from my mind so I had to start over. In the end I could achieve grade S1 (Sehr gut) without any problems. I can only say that the fear about FMI is highly exaggerated, if you study 150 hours = 6 ECTS then you shouldn't have any problems passing the exam. Most of the exams of the last 2 years were really fair and it is possible to pass them even with a good grade.

(SS20) I wouldn't be too quick to judge by your experience. Of course its possible to pass the exam and even get a good grade, but the fact that barely anyone ever gets a good grade and many people fail speaks for itself. The exams are already relatively difficult when you know more or less what you are getting. This isn't always the case, FMI profs/lecturers regularly give completely new problems in tests. Considering that the subject matter is already very extensive you have to be lucky to have learned or have knowledge on that new problem.

(SS20) Given prior knowledge and interest in the topic and actually doing all exercises conscientiously, about one week of intensive revising is more than enough to pass the exam with a good grade.

Unterlagen[edit]

  • Alte Prüfungsangaben und Notenstatistiken sind auf den Institutswebsites zu finden: dbai.tuwien.ac.at
  • 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 Block 1: Computational Complexity (Papadimitriou)
    • Buch für Block 2: Decision Procedures An Algorithmic Point of View (Kroening)
    • Buch für Block 3: The Science of Programming (Gries)
    • Buch für Block 4: Model Checking (Clarke)
  • Use the collaboratively formulated exam solutions

Tipps[edit]

  • Die alten Prüfungsangaben durchrechnen bereitet einen gut auf die Prüfung vor. Bei den Blöcken 1, 3 und 4 kommen immer ähnliche Beispiele. Für Block 2 (Satisfiability) gilt das leider nicht. Dort kann eigentlich alles verlangt werden, was Folien und Übungsblätter so her geben. 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 (ausgenommen Block 2).
  • 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?
  • 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.
  • 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).
  • (SS20)
    • Block 1: Study the slides and extra material on youtube. Try to understand all the complexity classes and reductions. Also study from excercise solutions and then try to solve past questions.
    • Block 2: Read the slides once and then study the exam solutions. Slides are impossible to understand and there is a lot of bla bla. Try to understand the solutions to past questions (like last 10-15 exams). I still have no idea what's going on in Block 2, I just memorized all the possible questions and their solutions. Pray Egly doesn't ask a new kind of question.
    • Block 3: Read the slides and listen to the lecture online where slides don't make sense. The lecturer helped me understand. Solve past questions. This block seems complicated at first but it is understandble.
    • Block 4: Read the slides once (dont try to understand whats going on). Only the slides 1 and 3 are relevant. Focus on solutions of past questions. Part a and b is always the same and should be easy points. Part c is also doable.
  • (SS20)
    • Ignore Block 2 for the beginning and focus on Block 1, 3 and 4 to avoid frustration. Especially Block 4 is quite easy. Study about 1 week per block, start with 1,3 and 4, then continue with 1 week repetition and continue with Block 2 followed by another week of repetition of all concepts and final exam preparation.
    • The best tipp to give is to ignore Block 2! Do not bother trying to understand Eglys stuff, I am quite sure he doesn't either ;). Jokes aside: Block 1, 3 and 4 are very much predictable even though sometimes Block 3 tends to diverge a little bit (see exam 16.10.2020). After you have done at least a couple of examples on Block 1, 3 and 4 then start learning for Block 2. It is not really predictable which examples he might give here so if you want a good score on this block you should consider going through all examples on the "Übungsblatt" and on the slides even though this takes some time. However DO NOT GIVE UP. It is more than just doable! I did not have any background in logic nor in complexity theory or any related topic and I was still able to score a "Sehr gut"!
  • (SS20/WS20): Teil 2 beim Lernen völlig ignoriert und auch 0 Punkte auf die Prüfung, Teil 1 auf Verständnis gelernt und alte Prüfungen gelernt, Teil 3 die alten Prüfungen gelernt und die Prüfungsrelevanten Dinge auf Verständnis gelernt, Teil 4 nur die 2 für die Prüfung relevanten Slides gelesen (1 und 3) und die Prüfungen durchgegangen und auf Verständnis komplett verzichtet. Hat für ein Genügend gereicht. Aufwand ca: ~2 Wochen moderates Lernen (VO Aufzeichnungen ansehen und verstehen, Prüfungen oberflächlich durchgehen) + ~10-14 Tage intensiveres Lernen (2 Wochen Urlaub genommen, die ~2 Wochen davor waren neben der Vollzeitarbeit). Bei den Übungsblättern habe ich die gemacht die so ähnlich waren wie die Prüfungsbeispiele.
  • (SS20/WS20) For all those who are worried: don't let yourself be discouraged by others saying the exam is too hard! I am not an expert in the topic and I would not judge it as easy, but with continuous preparation (recommendably around 1-2 months), it should be sufficient to pass it. RECOMMENDATION: Don't learn old exams by heart! Try to understand - even if this sounds not doable in the beginning, but understanding comes with time. Just take your time and do it. :)
  • (SS20) Some tips for part 2: Skipping it is a valid approach if one doesn't care about the grade. However, if you want to prepare, do the exercise (at least the recommended tasks) on your own and try your best to understand what is going on. Also try to come up with the proofs on your own, in this case you get valuable feedback for the exam's proves. Therefore, try to understand the feedback as well as the sample solution fully. Ask if you are uncertain. Although there are new exercises in part 2 regularly, there are still some patterns: exam exercises tend to repeat once in a similar fashion at the next exam, so have a look at the last two exams. Even if the exam tasks are new, they are often related to the exercises of that particular year. This is not always obvious, as it's not the task itself that is repeated but the underlying technique, proof structure, etc. Therefore, if you fully understand the exercises, you have a good chance to find the correct approach for the exam’s tasks. Learning anything by heart is a complete wast of time for this part (actually for all parts).

Verbesserungsvorschläge / Kritik[edit]

  • 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.
  • Schwierigste LVA im ganzen Masterstudium. Vorallem der Egly Teil (2) ist äußerst komplex und man hat das Gefühl, Egly glaubt Logik sei trivial.
  • Insteresting lecture for students of Logic and Computation and while part 1 and 3 are somehow relevant for others master programs, part 2 and 4 should be removed for non L&C students.

Attachments

Add new attachment