TU Wien:Formale Methoden der Informatik VU (Egly)

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

Daten[edit]

Lecturers Uwe EglyLaura KovacsMatthias KönigAnja Petkovic KomelSophie RainSarah Sophie SallingerFriedrich WeberStefan WoltranFlorian Zuleger
ECTS 6
Alias Formal Methods in Computer Science (en)
replaces Theoretische Informatik 2 VU (Baaz)
Department Logic and Computation
When summer semester
Last iteration 2022SS
Language English
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
SS21 25.06.2021 23.07.2021 28 Tage
SS21 22.10.2021 18.11.2021 27 Tage
SS21 10.12.2021 20.12.2021 10 Tage
WS21 21.01.2022 16.02.2022 26 Tage
WS21 25.03.2022 22.04.2022 28 Tage
SS22 24.06.2022 22.07.2022 28 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.

(SS21) Regardless of what people claim above, the exam shouldn't be taken lightly. The difficulty of the exams varies vastly. Relatively many of the recent ones contain exercises that you haven't seen before. I invested well over 150 hours and got a 4. I was quite nervous and made some stupid mistakes but at the same time my exam was IMO relatively easy.

(WS21) As with most lectures the time budget for this exam greatly depends on your prior knowledge. My Case: No prior knowledge, no informatics related bachelor just engineering --> I watched the lectures about 2-3 times which took me around 120-140 hours. Additional youtube videos and supplementary material through googeling to bridge the gaps in the lectures another 10-20 hours. Solving all exercises ~ 60 hours. Going through lecture slides a couple times ~ 30-40 hours. Solving past exams ~7-10 days á 6-8 hours/day (I felt it difficult to do these kind of exercises for prolonged amounts of time since it is rather complex especially at the beginning). Result: Passed at first attempt with Satisfactory. I am sure the lecture time can be reduced with prior knowledge and it depends how easily you can solve the exercises at the beginning so there surely is a good amount of wiggle room in the proposed time budget. All in all I'd say it was around 12 ECTS in time budget but that was to be expected for this lecture. I would thus recommend to not underestimate the time needed for this VU and perhaps not schedule it with the most difficult VUs in parallel.

(SS22) As a TU Vienna Software Engineering Bachelor graduate, I spent < 60 hours in total for a solid 2 on the first attempt. As always, efficient preparation in the form of solving old exams is key. I also watched all lectures, which would not really have been necessary.

(SS22) Maybe earlier exams were more difficult, but I can't at all understand some of the criticism displayed on this page. Yeah, it is a lot of material to learn and yeah, you kinda need to get lucky on the second part to get stuff you've known to get a good grade. But all in all I just fully focused for 10 days (5 days reading slides and understanding the example sheets, 5 days doing old exams) and got a really good B (if I went to the post-exam review I might've gotten an A, who knows). I get that the material might be difficult for some people, but all in all it's not a HUGE jump from the stuff learnt in Bachelor logics courses at TU Wien. I would not trust the claims of people above effectively learning for MULTIPLE MONTHS (?) and not getting a passing grade. They clearly did something wrong while learning or just overestimate the time they really spent learning as opposed to procrastinating.

(SS22) I feel like something about this course must have changed (Disclaimer: You can also check out the official grade statistics) - I don't get the comments of the previous students at all. I effectively studied for a week (exclusively, without any other things to do) for this exam. I did not really watch the lectures (except the parts I had problems while studying) and I did only do the first block of exercises (though in hindsight that was a very stupid idea!) - Total time spent maybe around 40-50 hours. Grade was a 3.

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).
  • (SS21) I'd recommend absolutely everybody who is not happy with their grade to have a post-exam review. I had to do the exam three times and every time I was wrongfully deducted 3-4 points.
  • (WS21) While I did study all blocks one after another (contrary to the advises above) I definietly spend most of the time on block 2 but got 2/15 points on the exam. Other blocks I got between 10-15 points so overall it was enough. However, one can see the deminishing returns with block 2 here so I can understand where others are coming from when they recommend to skip block 2 based on your grade preference/ time budget. For block 2 I'd recommend to do the exercises and hand them in (I believe that was my mistake as I appearently completely messed up the proofs according to Egly Feedback on the exam. I was pretty confident I got it right straight after the exam but that proofed to be false so doing the exercises for block 2, handing them in and getting a feeling for what Egly wants you to do might be a better strategy here). For Blocks 3,4 the past exams were the best preparation for me, at some point you get the hang of it (Provided they don't change the exam structure from the prior 3 years 2019-2022). Block 1 was actually done well in the lecture material so I'd recommend to go through that and solving exam exercises in parallel (They show signs of repetitions after certain years).

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.
  • From a didactical perspective the course is a catastrophe. Some topics (especially in block 2) are barely or very badly explained but need to be understood in detail to avoid getting deducted large amounts of points during the exam. Knowledge that is critical for the exam is often difficult to find in the slides. Sometimes exercises that even the lecturers/tutors have a hard time explaining in reasonable time are given in an exam. Relatively many of the exams contain exercises that are accidentally contradictory, wrong (there is an exercise in a 2018 exam that directly contradicts the slides) or very badly formulated. In contrast to that you can easily get deducted large amounts of points for small errors, which gives you the feeling that there is a certain hypocrisy. The situation is not made better by the fact that four professors, each with different grading standards, work on the exams. Egly, for example, happily deducts relatively large numbers of points for imprecise/slightly incorrect solutions, while imprecision and slight incorrections are handled much more forgiving in the other blocks. Overall, I had the feeling that the course is much about gambling for a reasonable exam and less about actual knowledge. During the course you occasionally hear from the lecturerers/tutors that "oh the students don't want to learn" or that "the students just want to learn this by heart, you can't do this here, you have to understand it". IMO the lecturers/tutors are shifting the blame for an unnecessarily large number of failing students while avoiding to meaningfully improve the course. A friend of mine and me found the course very difficult (especially finding out whether a theory we had on the subject matter was true or not) despite always being in the top 10% of students and always learning by understanding the subject matter. That being said, looking at previous material, there have certainly been several considerable improvements (e.g. making the exercises in the exam less a hit or miss) in the last few years.
  • 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.
  • It should follow the exam mode of Bachelor courses with the exercises counting towards points of the final grade but not being mandatory to pass the course. If it was like this, the course would be fine as it is.

Attachments

Add new attachment