Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2016 / Formale Spezifikation und Verifikation


Inhaltsbereich

Formale Spezifikation und Verifikation

Vorlesung, 3-std., Mo 12-14, Mi 16-18, Schöpp; Übungen 2-std., Schöpp

Aktuelles

  • Einsicht Nachklausur: Mittwoch, den 16.11., 17-18 Uhr, Raum L109 Oettingenstr.
  • Die Nachklausur findet am 11.10. statt. Bitte melden Sie sich bis zum 27.9. bei UniWorX an.
  • Die Anmeldung zur Klausur ist noch bis zum 13.7. möglich.
  • Blatt 10 wurde aus Versehen nur in UniWorx und im git-Repository veröffentlicht. Es ist nun auch hier verlinkt.
  • Gastvortrag: Keiko Nakata von FireEye Inc.
    Thema: Überblick über die praktische Anwendung formaler Methoden bei FireEye 
    Mittwoch, 29.6., 10 Uhr, Raum D 018, Richard-Wagner-Str. 10

  • Die Donnerstagsübung am 26.5. entfällt (Fronleichnam). Die Mittwochsübung am 25.5. findet statt und kann als Fragestunde oder zur Bearbeitung von Blatt 5 genutzt werden. Blatt 5 wird in der Woche vom 30.5. besprochen.

  • Am 18.5. entfällt planmäßig die Vorlesung. Die Übungen finden dennoch zu regulären Zeit und am regulären Ort statt (Mi 18-20 Uhr, Do 10-12 Uhr).
  • Die Donnerstagsübung am 5.5. entfällt (Himmelfahrt). Die Mittwochsübung am 4.5. findet als allgemeine Fragestunde statt. Blatt 3 wird erst in der Woche vom 9.5. besprochen.
  • Bitte beachten Sie die Planung der Vorlesungstermine.
  • Bitte melden Sie sich bei UniWorx für die Vorlesung an.

Inhalt

In der Vorlesung werden Spezifikationsformalismen, Konzepte der Systemmodellierung, Grundtechniken für die Automatisierung der Verifikation, Typsysteme und statische Analyse eingeführt.


Organisation


Zeit und Ort

VeranstaltungZeitOrtBeginn
Vorlesung Mo, 12–14 c.t. Geschw.-Scholl-Pl. 1, B 106 18.04.2016
Vorlesung Mi, 16–18 c.t. Geschw.-Scholl-Pl. 1, A 125 20.04.2016
Übung Mi, 18–20 c.t. Amalienstr. 73a, Raum 211 20.04.2016
Übung Do, 10–12 c.t. Edmund-Rumpler-Strasse 13, B 257 21.04.2016

Planung

Da die Vorlesung trotz der zwei wöchentlichen Vorlesungstermine insgesamt nur den Umfang von 3 SWS hat, findet die Vorlesung nicht an allen Terminen statt. Der vorläufige Zeitplan ist unten angegeben. Die Übungen finden durchgehend wöchentlich statt.

Nr.DatumThemaHinweise
11.4.
13.4.
1. 18.4 Organisation, Aussagenlogik: Syntax und Semantik, Modellierung von Sudoku
2. 20.4. Aussagenlogik
3. 25.4. Aussagenlogik
4. 27.4. BDDs
5. 2.5. BDDs
6. 4.5. Temporallogik: CTL, Model Checking
7. 09.5. Model-Checking-Algorithmen
8. 11.5. SMV, Fairness
16.5. Pfingstmontag
18.5.
9. 23.5. Alternating Bit Protocol
10. 25.5. Symbolic Model Checking, Programmanalyse: Einführung, Induktive Definitionen
11. 30.5. Spezifikation einer while-Sprache: Syntax, operationelle Semantik
12. 1.6. Datenflussanalyse (Liveness, Reaching Definitions, Available Expressions)
13. 6.6. Fixpunkttheorie
8.6.
13.6.
14. 15.6. Datenflussanalyse und Typsysteme
15. 20.6. Einfache funktionale Sprache: operationelle Semantik, Typsystem
16. 22.6. Typinferenz mit Algorithmus W und Unifikation
17. 27.6. Typ- und Effekttypsysteme: Kontrollfluss, Referenzen
18. 29.6. Typ- und Effekttypsysteme: Exceptions
19. 4.7. Zusammenfassung und Ausblick; Hoare Logik
20. 6.7. Wiederholungs- und Fragestunde
11.7.
13.7.

Materialien

Alle Materialien und Übungen finden Sie in auch in folgendem git-Repository.


  • Blatt 1 (Aussagenlogik) – Besprechung in der Woche vom 18.4.
  • Blatt 2 (Aussagenlogik und SAT) – Abgabe bis 27.4; Besprechung in der Woche vom 25.4.
  • Blatt 3 (BDDs) – Abgabe bis 11.5; Besprechung in der Woche vom 9.5.
  • Blatt 4 (CTL)Abgabe bis 18.5; Besprechung in der Woche vom 16.5.
  • Blatt 5 (SMV) – Abgabe bis 1.6; Besprechung in der Woche vom 30.5.
    • Die SMV-Dateien aus den Übungen finden Sie hier.
  • Blatt 6 (symb. Model Checking, Programmanalyse) – Abgabe bis 8.6.; Besprechung in den Woche vom 6.6. und 13.6.
  • Blatt 7 (Programmanalyse) – Abgabe bis 13.6.; Besprechung in den Wochen vom 13.6. und 20.6.
  • Blatt 8 (Typsystem für Programmanalyse) – Abgabe bis 22.6.; Besprechung in der Woche vom 20.6.
  • Blatt 9 (Funktionale Sprache, Typsystem) – Abgabe bis 29.6.; Besprechung in der Woche vom 27.6.
    • Ein Interpreter für die einfache funktionale Sprache ist am CIP-Pool installiert. Er kann auf der Kommandozeile mit dem Kommando /home/sch/schoepp/bin/fun ausgeführt werden. Zur Benutzung siehe folgende Beispielsitzung.
    • Beispiellösungen: Aufgabe 9-1, Aufgabe 9-4 a)
  • Blatt 10 (Typsysteme)  – Abgabe bis 6.7.; Besprechung in der Woche vom 4.7.
  • Blatt 11 (Wiederholung einiger Teile der Kapitel 1 und 2)

Literatur


Klausur

Klausur

  • Termin: Mittwoch 27.07., 10-13 Uhr
  • Bearbeitungszeit: 120 Minuten

Nachklausur

  • Termin: Dienstag 11.10., 9-12 Uhr
  • Ort: Hörsaal A 240 (HGB)
  • Beginn: 9:15 Uhr
  • 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.
    Sollte in einer Klausuraufgabe eine Herleitung verlangt sein, so werden die entsprechenden Regeln auf einem Zusatzblatt angegeben sein. Möglich sind aber auch Aufgaben zum Regelverständnis, siehe z.B. Aufgabe 9-3, in der sinnvolle Regeln anzugeben waren. Sie brauchen die Regeln also nicht auswendig zu lernen, sollten sie aber inhaltlich verstehen, erklären und anwenden können. Natürlich kostet es auch Zeit, wenn man beim Herleiten jede Regel einzeln nachschlagen muss. Eine gute Übung zum Verständnis der Regeln ist auch, einzelne Regeln ohne Nachschlagen mit etwas Nachdenken zu rekonstruieren.
  • Mitzubringen sind:
    • gültiger Immatrikulationsnachweis für dieses Semester
    • gültiger Personalausweis oder Pass mit Lichtbild
    • Schreibzeug (keine Rot- und Grünstifte, kein Bleistift)
    • Eigenes Papier ist nicht erforderlich und darf für die Prüfung nicht benutzt werden.

Artikelaktionen


Funktionsleiste