TU Wien:Computer Aided Verification VU (Veith)

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.

Daten

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	Prof. Veith
ECTS	3
Sprache	English

Zuordnungen

Masterstudium Logic and Computation
Masterstudium Technische Informatik

Inhalt

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

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

Logik und Graphentheorie ist hilfreich aber nicht unbedingt notwendig

Vortrag

Etwas konfus wodurch man leicht den Faden verliert.

Übungen

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

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

noch offen

Zeitaufwand

noch offen

Unterlagen

Model Checking (Clarke, Grumberg, Peled)

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) - Book - Model Checking - E. M. Clarke.djvu

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

• Materialien

Tipps

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

noch offen

Materialien

Neues Material hinzufügen

P

• Prüfung 28.6.2013
• Prüfung 29.6.2012