TU Wien:Computer Aided Verification VU (Veith)

Aus VoWi
Wechseln zu: Navigation, Suche

Daten[Bearbeiten]


Inhalt[Bearbeiten]

Laut Tuwis:

Modellierung von Hardware und Software, Überblick über computerunterstuetzte Verifikationsmethoden. Spezifikation durch Temporallogik und Automaten, Simulation und Bisimulation, Zustands-Explosion, explizite und symbolische Model Checking Verfahren, Abstraktion und Abstraktionsverfeinerung, Predicate Abstraction, Entscheidungsprozeduren, Beweisertools. Verifikationssoftware in der Praxis, Überblick über Verifikation spezieller Systeme und aktuelle Entwicklungen.

Erfahrung: Es werden einige Logiken für Model Checker vorgestellt und es wird gezeigt wie man durch geschickte Wahl der Datenstrukturen den Problembereich soweit minimiert, dass er lösbar wird. Der Teil über die praktische Anwendung der Model Checker ist verschwindend klein und 90%+ der Zeit wird für die vorher genannten Punkte aufgewendet.

Ablauf[Bearbeiten]

Geblockt an 3 Tagen (auch Wochenende)

SS12: Fr. 2-6 (5 Termine oder so)

SS14: Freitags 14:00 bis 15:00 geblockt von 4.April bis Ende des Semesters. Es wurde auch angekündigt das er mehrfach nicht anwesend sein wird, weshalb er 3 statt 2 Stunden eingeplant hat. (Im ECTS Breakdown sind nämlich nur 25 Vorlesungsstunden eingetragen)

Benötigte/Empfehlenswerte Vorkenntnisse[Bearbeiten]

Logik und Graphentheorie ist hilfreich aber nicht unbedingt notwendig

Vortrag[Bearbeiten]

Etwas konfus wodurch man leicht den Faden verliert.

Übungen[Bearbeiten]

Im SS09 waren 9 Beispiele auszuarbeiten wovon mindestens 6 für eine "optimale" Note gelöst werden müssen. Die Beispiele sind wie die LVA generell theoretischer Natur. (Beweise, logische Ausdrücke umwandeln, Binary Decision Diagram bzw. Kripke Struktur zu einem Ausdruck finden etc.)

Im SS14 hat er mehrere Exercises angekündigt, die Lösung der Beispiele kann bis zu 10 Prozentpunkte auf den Test/die Prüfung gut geschrieben werden. Die Übungen sind freiwillig zu lösen und die gelösten Beispiele sind beim Test oder der Prüfung abzugeben.

Prüfung, Benotung[Bearbeiten]

Schriftlicher Termin Ende des Semesters. Nachher mündliche Prüfungen nach Vereinbarung. (Da Prof. Veith nicht in Wien lebt können diese Termine nur recht sporadisch mit größeren Zeitabständen angeboten werden) SS 11: Mündl. Prüfung direkt nach VO.

Für eine positive Note müssen die Hälfte der möglichen Testpunkte geschafft werden. Bei der mündlichen Prüfungen muss der Eindruck entstehen das man sich auskennt und sich mit dem Thema beschäftigt hat.

Fragestellung:

  • Was ist Bounded Model Checking?
  • Wie checkt man zB EF(q U p) mit OBDD (RelProd, etc.)

Benotung: Sehr human. Übung kann die Note aber verbessern/ausbügeln.

Dauer der Zeugnisausstellung[Bearbeiten]

noch offen

Zeitaufwand[Bearbeiten]

noch offen

Unterlagen[Bearbeiten]

Model Checking (Clarke, Grumberg, Peled)[Bearbeiten]

  1. Büchereilink: "Model Checking" von Clarke, Grumberg, Peled
  2. ISBN 0-262-03270-8
  3. Vowi: Datei:TU Wien-Formale Methoden der Informatik VU (Egly) - Model Checking - E. M. Clarke.djvu

Folien welche im TISS unter Unterlagen für das SS12 und früher auffindbar sind.

Tipps[Bearbeiten]

Anwesenheit da die Folien nicht alles abgedecken. Es ist auch sinnvoll die Folien vorher auszudrucken und mitzubringen da der Vortrag von den Folien stark entkoppelt ist und viele Folien einfach überspringt obwohl sie behandelt werden.


Verbesserungsvorschläge / Kritik[Bearbeiten]

noch offen