Spezifikation und Verifikation
Vorlesung, 3-std., Mo 10-12, Do 10-12, Hofmann; Übungen 2-std., Schöpp
Aktuelles
- Die Anmeldung zur Nachholklausur am 14.4. ist nun über UniWorX möglich (bis 11.4.).
Inhalt
In der Vorlesung werden Spezifikationsformalismen, Konzepte der Systemmodellierung, Grundtechniken für die Automatisierung der Verifikation, Typsysteme und statische Analyse eingeführt.
Organisation
- Umfang: 3+2 Semesterwochenstunden
- Vorlesung: Prof. Dr. Martin Hofmann
- Übungen: Dr. Ulrich Schöpp, Julien Oster
Zeit und Ort
| Veranstaltung | Zeit | Ort | Beginn |
| Vorlesung | Mo, 10–12 c.t. | Hörsaal B005 (Theresienstr. 39) | 26.10.2009 |
| Vorlesung | Do, 10–12 c.t. | Hörsaal B005 (Theresienstr. 39) | 29.10.2009 |
| Übung | Fr, 10–12 c.t. | Hörsaal B041 (Theresienstr. 39) | 30.10.2009 |
| Übung | Fr, 12–14 c.t. | Hörsaal B041 (Theresienstr. 39) | 30.10.2009 |
Die Vorlesung findet an den folgenden Terminen statt: 26.10.09, 29.10.09, 09.11.09, 12.11.09, 16.11.09, 19.11.09, 23.11.09, 26.11.09, 30.11.09, 03.12.09, 07.12.09, 10.12.09, 14.12.09, 11.01.10, 14.01.10, 25.01.10, 28.01.10, 01.02.10, 04.02.10, 08.02.10
Log
| Termin | Stoff | Folien | Sonstiges |
| 26.10. | Organisatorisches, Aussagenlogik, Beispiel: Sudoku | 1-27 | |
| 29.10 | Tseitin Übersetzung, Sat-Solver, DPLL-Algorithmus mit Klausellernen, Modellierung von Addierwerken | 28-48 | |
| 3.11. | keine Vorlesung | ||
| 5.11. | keine Vorlesung | ||
| 9.11. | Modellierung nebenläufiger Systeme in Aussagenlogik mit Sat-Solver. | 49-51 | |
| 12.11. | Wdh Peterson mit SAT Solver. BDDs Grundlegende Definitionen | 51-66 | |
| 16.11. | BDDs Grundalgorithmen und Implementierung, Modellierung nebenl. Systeme mit BDDs | 67-79 | |
| 19.11. | Wdh Mod. mit BDDs. Einf. Model-Checking CTL Syntax&Semantik | 80-95 | |
| 23.11. | Model-Checking Algorithmus fuer CTL | 96-105 | |
| 26.11. | Das System SMV | 106-126 | |
| 30.11. | Model Checking mit Fairness, Alternating Bit Protokoll | 127-135 | |
| 3.12. | ABP fertig (s.u.), Symbolisches Model-Checking, LTL, Definition Buechi-Automat | 136-148 | |
| 7.12. | Buechi Automaten, Model-Checking mit Buechi Automaten, SPIN, Kapitel 3 Motivation | 149-163 | |
| 10.12. | Programmanalyse: Reaching Definitions, Gleichungs- und Constraintbasiert. Available Expressions. | 164-177 | |
| 14.12. | Datenflussgleichungen, Liveness von Variablen, groesste/kleinste Loesung. Typsystem fuer Reaching Definitions | 178-187 | |
| 17.12. | keine Vorlesung | ||
| 21.12. | keine Vorlesung | ||
| 7.1. | keine Vorlesung | ||
| 11.1. | Wdh. Semantische Korrektheit von Programmanalysen mit Typsystemen. Operationelle Semantik | 188-192 | |
| 14.1. | Wdh. Funktionale Sprache, einfaches Typsystem. Typinferenz mit Beispielen. | 193-201 | |
| 18.1. | keine Vorlesung | ||
| 21.1. | keine Vorlesung | ||
| 25.1. | Typinferenz fuer einfaches und polymorphes Typsystem. Kontrollflussanalyse (nur Motivation). | 202-215 | |
| 28.1. | Typsysteme fuer Kontrollflussanalyse und Seiteneffekte. Effektsystem im allgemeinen, Subtyping | 216-229 | |
| 1.2. | Typ- und Effektsystem fuer Exceptions, Zusammenfassung Typsysteme | 230-239 | |
| 4.2. | Klausurwiederholung | ||
| 8.2. | Klausurwiederholung / Hoare Logik mit rekursiven Prozeduren |
Materialien
- Folien Kapitel 1 (pp 1–79) (letzte Änderung 16.11.09, 00:48)
- Folien Kapitel 2 (pp 79–157) (letzte Änderung 03.12.09, 09:53)
- OCaml Programme cnf.tgz, zur Benutzung mit dem Sat-Solver zChaff. Enthält auch die Beispiele adder.ml, sema.ml, peterson.ml, wolf.ml (letzte Änderung 16.11.09, 15:19)
- Sat-Solver und Tseitin-Transformation in Java, analog zu obigem OCaml Program: javaCNF.zip (enthält den Sat-Solver SAT4J) (letzte Änderung 24.11.09, 17:47)
- OCaml Programme bdd.tgz, fuer BDDs. Verwendet CUDD und MLCUDDIDL. Enthält auch die Beispiele adder.ml, sema.ml, peterson.ml (diesmal mit BDDs) (letzte Änderung 16.11.09 00:58).
Eine im CIP-Pool lauffähige Version dieser Programme mit allen Bibliotheken liegt im Verzeichnis /home/sch/schoepp/bdd. - NuSMV Beispieldateien aus der Vorlesung. bspnusmv.tgz (26.11.09, 09:36)
- Alternating Bit Protokoll: wie in der Vorlesung, Alternative Loesung
- Folien Kapitel 3 (158-239) (letzte Aenderung 04.02.10, 09:50)
Übungen
- Blatt 1
- Blatt 2 (Beispiellösung: javaCNF.zip)
- Blatt 3
- Blatt 4 (Die in Aufgabe 13 gefragten Eigenschaften kann man mit NuSMV prüfen: aufgabe13.smv)
- Blatt 5
- Blatt 6
- Blatt 7 (aufgabe25.zip, aufgabe26.pdf, aufgabe28.ml berechnet die Lösung für Aufgabe 28)
- Blatt 8 (aufgabe29.ml berechnet die Lösung für Aufgabe 29, letzte Änderung 4.2., aufgabe31.pdf)
- Blatt 9 (aufgabe35.pdf, aufgabe36.pdf, aufgabe39.pdf)
- Blatt 10 (aufgabe40.pdf)
- Blatt 11
Literatur
- Huth, Ryan. Logic in Computer Science, Cambridge University Press, 2004
- Nielson, Nielson, Hankin. Principles of Program Analysis, Springer, 2005
Klausur
Erstklausur: Dienstag 16.2. 10–13 Uhr, Hörsaal A140 (Hauptgebäude, 1.Stock, Raumplan (Mitte oben))
- Bearbeitungszeit: 120 Minuten
- Die Klausur findet ohne Hilfsmittel statt. Insbesondere sind keine schriftlichen Unterlagen, keine Taschenrechner oder andere Rechner, keine Mobiltelefone oder andere Kommunikationsmittel erlaubt.
- Erforderliche Unterlagen:
- gültiger Immatrikulationsnachweis für dieses Semester
- gültiger Personalausweis oder Pass mit Lichtbild
- Schreibzeug
- Eigenes Papier ist nicht erforderlich und darf für die Prüfung nicht benutzt werdenE
- Ergebnis (inkl. Notenbonus)
- Einsicht: Freitag 5.3. 14–15 Uhr, Oettingenstraße 67, Z1.09 (neu L109)
Nachholklausur: Mittwoch 14.4. 14–17 Uhr, Hörsaal A240 (Hauptgebäude)
- Ergebnis (inkl. Notenbonus)
- Einsicht: Freitag 7.5. 13:15–14:15 Uhr, Oettingenstraße 67, U169
