TU Wien:Computer Aided Verification VU (Weissenbacher)
- Computer Aided Verification VU (Cerny) (TU Wien, 0 Materialien)
- Computer Aided Verification VU (Weissenbacher) (TU Wien, 6 Materialien)
- Computer Aided Verification LU (Veith) (TU Wien, veraltet, 0 Materialien)
- Computer Aided Verification UE (Weissenbacher) (TU Wien, veraltet, 0 Materialien)
- Computer Aided Verification VU (Veith) (TU Wien, veraltet, 2 Materialien)
Daten[Bearbeiten | Quelltext bearbeiten]
| Vortragende | Georg Weissenbacher |
|---|---|
| ECTS | 3 |
| Letzte Abhaltung | 2022W |
| Sprache | English |
| Abkürzung | CAV |
| Mattermost | computer-aided-verification • Register • Mattermost-Infos |
| Links | tiss:181145, eLearning |
| E066011 | |
| Masterstudium Logic and Computation | |
| Masterstudium Software Engineering & Internet Computing | |
| Masterstudium Technische Informatik |
Inhalt[Bearbeiten | Quelltext bearbeiten]
Prinzipiell besteht die Vorlesung aus einer Einführung in verschiedene Model Checking Techniken, unter anderem: Explicit State Model Checking, Symbolic Model Checking, Bounded Model Checking und Interpolation-based Model Checking. Zu Beginn geht es eher um die Grundlagen, das heißt SAT Solving, Binary Decision Trees / Diagramme und Kripke Strukturen und später werden neben den verschiedenen Techniken auch Tools wie z.B. Promela / Spin oder (Nu)SMV vorgestellt.
Gegen Ende des Vortrags kommt ein oder zwei Übungsblätter online, die optional sind. Da es allerdings Zusatzpunkte für die Abschlussprüfung bringt, und die Übungsblätter eine gute Vorbereitung für die Prüfung sind, empfiehlt es sich sehr ausreichend Zeit in diese zu investieren. Nach Abschluss des Vortrages wird die jeweilige Übungsaufgabe für die Computer Aided Verification UE vorgestellt, die dann über den Sommer abgeschlossen werden kann.
Ablauf[Bearbeiten | Quelltext bearbeiten]
S2016: Geblockte Abhaltung der Vorlesungen an den Freitagen des zweiten Teils des Sommersemesters, Ungefähr nach der Hälfte der Vorträge wurde ein Übungsblatt online gestellt das bis Semesetrende abzugeben ist (optional), Schriftliche Prüfung am Ende des Semesters, oder eine mündliche Prüfung die Student_innen sich per Mail ausmachen.
Benötigte/Empfehlenswerte Vorkenntnisse[Bearbeiten | Quelltext bearbeiten]
Es lohnt sich schon etwas über SAT Solver und Fixpunkte gehört zu haben, prinzipiell geht es aber auch ohne diese Vorkenntnisse.
Vortrag[Bearbeiten | Quelltext bearbeiten]
Der Vortrag war von allen drei Vortragenden (Weißenbacher, Konnov, Widder) sehr bemüht. Das Klima war sehr freundlich, es war kein Problem (auch grundlegende) Fragen zu stellen.
Die Erklärungen wurden bei Bedarf durch Beispiele auf den Folien oder an der Tafel ergänzt.
Übungen[Bearbeiten | Quelltext bearbeiten]
Im S2016 gab es eine Exercise Session, in der ein Tutor Beispiele eines Übungsblatts erklärt hat. Da die Beispiele am Übungsblatt sehr ähnlich waren, zahlt es sich aus diese Session zu besuchen.
Für die Bearbeitung des Übungsblatts sind ca. 4 Wochen Zeit. Dieses kann dann entweder im TUWEL hochgeladen, im Sekretariat abgegeben, oder einfach zur Prüfung mitgenommen werden.
Der Tutor stand auch abseits der Exercise Session für Fragen per Mail oder persönlich im Büro (dessen Örtlichkeit ich allerdings zuerst per Mail erfragen musste) sehr hilfreich zur Verfügung.
Prüfung, Benotung[Bearbeiten | Quelltext bearbeiten]
Entweder schriftlich am Ende des Semesters, die Beispiele waren ähnlich zu den Übungsblättern und Unterlagen sind erlaubt. Oder mündlich nach Terminvereinbarung.
Laut Erzählungen wird eher nach Verständnis gefragt, es ist vertretbar wenn nicht jeder Algorithmus im Detail erklärt werden kann.
Dauer der Zeugnisausstellung[Bearbeiten | Quelltext bearbeiten]
Ca. 4 Wochen
Zeitaufwand[Bearbeiten | Quelltext bearbeiten]
Wöchentlicher Vortrag der 2-3 Stunden dauert. Für das Übungsblatt sollten schon 10 bis 20 Stunden einrechnet werden, je nachdem wieviele Beispiele geplant sind und wieviel Vorwissen mensch mitbringt.
Falls Student_innen motiviert sind, empfiehlt es sich auch in das sehr gute Model Checking Buch von Ed Clarke et. al. reinzuschauen und wöchentlich 1-2 Stunden in das Lesen von Hintergrund Material zu investieren um sich auf die Vorlesungen vorzubereiten.
Unterlagen[Bearbeiten | Quelltext bearbeiten]
Buch: Model Checking (Ed Clarke et.al.)
Tipps[Bearbeiten | Quelltext bearbeiten]
- Macht auf alle Fälle die Übungsblätter - sie helfen euch beim Bestehen der Lehrveranstaltung
- Besucht (wenn möglich) die im Vergleich zu anderen LVAs sehr guten Vorlesungen
- Bei Problemen mit den Übungsblättern fragt nach
Highlights / Lob[Bearbeiten | Quelltext bearbeiten]
noch offen
Verbesserungsvorschläge / Kritik[Bearbeiten | Quelltext bearbeiten]
S2016: Der Vortrag hat teilweise unstrukturiert gewirkt, es war nicht immer klar wo Themen in das große und ganze passen. Organisatorische Details (wie Ablauf der Übungen, Anzahl der Punkte für Übungsblätter oder Termine) waren nur schleppend verfügbar, das liegt vermutlich an der sehr kurzfristigen Übernahme der Lehrveranstaltung. Es ist anzunehmen das die Organisation und die Struktur S2017 bessser wird.