TU Wien:Computer Aided Verification UE (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 Weißenbacher |
|---|---|
| ECTS | 3 |
| Sprache | English |
| Abkürzung | CAV |
| Links | tiss:181144 |
| Masterstudium Logic and Computation | |
| Masterstudium Software Engineering & Internet Computing | |
| Masterstudium Technische Informatik |
Mattermost: Channel "computer-aided-verification" • Register • Mattermost-Infos
Inhalt[Bearbeiten | Quelltext bearbeiten]
Entwickeln eines eigenen Model-Checkers für Gatterschaltungen bestehend ausschließlich aus UND-Gattern. Das Input-Format ist öffentlich verfügbar und es gibt dazu gute Dokumentation und existierende Tools. Außerdem gibt es eine offizielle Sammlung von Beipspieldateien die auch für das Abgabegespräch verwendet werden. Der Checker soll überprüfen ob die Schaltung safe ist, Gegenbeispiele müssen nicht gefunden werden. Dazu hat man nur Minisat verfügbar, alles andere muss selbst implementiert werden.
Ablauf[Bearbeiten | Quelltext bearbeiten]
Eine Vorbesprechung in der letzten Vorlesung der dazu passenden VU. Es gibt einen Foliensatz der die Angabe beschreibt und kurz die nötigen Details von Minisat beschreibt. Dann Entwicklung des Model-Checkers in einer beliebigen Programmiersprache (zeitlich meist über die Sommerferien). Wenn diese abgeschlossen ist wird individuell ein Abgabegespräch vereinbart wo einige der Testfälle durchprobiert werden und die Implementierung erklärt werden muss.
Benötigte/Empfehlenswerte Vorkenntnisse[Bearbeiten | Quelltext bearbeiten]
Das Wissen aus der dazu passenden VU (zumindest der eine Foliensatz mit Interpolation based Model Checking) ist unbedingt notwendig. Grundlegende C++ Kenntnisse von Vorteil, denn auch wenn man selbst jede Sprache verwenden darf ist MiniSAT in C++ geschrieben.
Vortrag[Bearbeiten | Quelltext bearbeiten]
Gibt es keinen.
Prüfung, Benotung[Bearbeiten | Quelltext bearbeiten]
Ein Abgabegespräch. Sehr entspannte Atmosphäre. Wenn man alles sauber implementiert hat und die Theorie verstanden hat ist das nur eine Formalität. Für ein Genügend reicht es angeblich nur den ersten Teil der Aufgabe (Bounded Model Checker) zu implementieren.
Dauer der Zeugnisausstellung[Bearbeiten | Quelltext bearbeiten]
Unmittelbar nach dem Abgabegespräch.
Zeitaufwand[Bearbeiten | Quelltext bearbeiten]
Nicht zu unterschätzen, aber definitiv im Rahmen von 3 ECTS. Da man nur MiniSAT zur Verfügung hat, müssen auch andere elementare Elementare Teile (z.B. Tseitin-Transformation) selbst geschrieben werden.
Unterlagen[Bearbeiten | Quelltext bearbeiten]
noch offen
Tipps[Bearbeiten | Quelltext bearbeiten]
Einige existierende Model Checker können das AIG Format lesen. Damit kann man überprüfen, ob der eigene Model Checker die richtigen Antworten liefert.
Verbesserungsvorschläge / Kritik[Bearbeiten | Quelltext bearbeiten]
noch offen