TU Wien:Computer Aided Verification UE (Weissenbacher)

Aus VoWi
Wechseln zu: Navigation, Suche
Ähnlich benannte LVAs (Materialien):

Daten[Bearbeiten]

Vortragende Georg Weißenbacher
ECTS 3
Abteilung Forschungsbereich Formal Methods in Systems Engineering
Wann Sommersemester
Sprache English
Links tiss:181144
Zuordnungen
M. Logic and Computation Wahlmodul Programming Languages and Verification
M. Software Engineering & Internet Computing Wahlmodul Formale Methoden und Theoretische Informatik
M. Technische Informatik Wahlmodul Computer-Aided Verification

Mattermost: Channel "computer-aided-verification" Team invite & account creation link Mattermost-Infos

Inhalt[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]

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]

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]

Gibt es keinen.

Prüfung, Benotung[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]

Unmittelbar nach dem Abgabegespräch.

Zeitaufwand[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]

noch offen

Tipps[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]

noch offen

Materialien

Diese Seite hat noch keine Materialien, du kannst aber neue hinzufügen.