TU Wien:Computer Aided Verification UE (Weissenbacher)

Aus VoWi
Zur Navigation springen Zur Suche springen
Ähnlich benannte LVAs (Materialien):

Daten[Bearbeiten | Quelltext bearbeiten]

Diese LVA wird nicht mehr von dieser Person angeboten, ist ausgelaufen, oder läuft aus und befindet sich daher nur noch zu historischen Zwecken im VoWi.
Vortragende Georg Weißenbacher
ECTS 3
Sprache English
Abkürzung CAV
Links tiss:181144
Zuordnungen
Masterstudium Logic and Computation
Masterstudium Software Engineering & Internet Computing
Masterstudium Technische Informatik

Mattermost: Channel "computer-aided-verification"RegisterMattermost-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

Materialien

Diese Seite hat noch keine Anhänge, du kannst aber neue hinzufügen.