Links und Funktionen
Sprachumschaltung

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


Inhaltsbereich

Formale Spezifikation und Verifikation

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

Aktuelles

  • Der Termin für die Nachholklausur steht jetzt fest. Die Anmeldung ist bis zum 21. September bei UniWorx möglich.
  • Klausureinsicht: Dienstag, 19.8., 13-14 Uhr, Raum L109 Oettingenstr. 67

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

Veranstaltung  Zeit  Ort Beginn
Vorlesung Mo, 12–14 c.t. Oettingenstr. 67, BU101 07.04.2014
Vorlesung Mi, 16–18 c.t. Oettingenstr. 67, BU101 09.04.2014
Übung Mi, 18–20 c.t. Ludwigstr. 25, E 021 23.04.2014
Übung Do, 10–12 c.t. Geschw.-Scholl-Pl. 1 (M), M 001 24.04.2014

Planung

Da die Vorlesung trotz der zwei wöchentlichen Vorlesungstermine insgesamt nur den Umfang von 3 SWS hat, findet die Vorlesung nur an den unten angegebenen Terminen statt. Die Übungen finden durchgehend wöchentlich statt.

Vorläufige Vorlesungsplanung

Nr. Datum Thema Dozent Hinweise
1. 7.4.

Organisation, Aussagenlogik: Syntax und Semantik, Modellierung

von Sudoku.

MH Folien 1-23
2. 9.4. Aussagenlogik MH Folien 24-33
3. 14.4 Aussagenlogik US Folien 34-49
4. 16.4. BDDs US Folien 50-62
21.4. keine Vorlesung (Ostermontag)
5. 23.4. BDDs MH Folien 63-78
28.4. keine Vorlesung
30.4. keine Vorlesung
5.5. keine Vorlesung
7.5. keine Vorlesung
6. 12.5. CTL, Model Checking MH Folien 79-96
7. 14.5. Model-Checking-Algorithmen MH Folien 97-108
8. 19.5. SMV, Fairness MH Folien 109-129
9. 21.5. Alternating bit protocol MH

Folien 130-135

Implementierung während der Vorlesung.

10. 26.5. LTL und Buchi Automaten. Programmanalyse: Motivation und erste Definitionen. MH Folien 136,142-157,159-165
11. 28.5. Programmanalyse: Reaching Definitions, Available Expressions MH Folien 166-182
12. 2.6. Fixpunkttheorie MH Folien 182-185
4.6. keine Vorlesung
9.6. keine Vorlesung (Pfingstmontag)
13. 11.6. Live Variablen, Einfache funktionale Sprache, einfaches Typsystem MH Folien 186-190, 203-206
14. 16.6. Typinferenz mit Algorithmus W und Unifikation MH Folien 207-213
15. 18.6. Typ- und Effektsyteme: Exceptions und Referenzen MH Folien 214-233
23.6. keine Vorlesung
25.6. keine Vorlesung
16. 30.6. Hoare Logik: Grundlagen US
17. 2.7. Hoare Logik: Methoden und Prozeduren US
18. 7.7. Ausblick: JML (Java Modelling Language) US
19. 9.7. Klausurwiederholung

Materialien

Eine Übersicht über alle Materialien finden Sie hier.


Übungen

 


Literatur


Klausur

Bitte beachten Sie die Hinweise zur Neuregelung für die Dokumentation der Prüfungen.

Erstklausur

  • Termin: Montag, 28. Juli 2014, 10-13 Uhr
  • Raumaufteilung nach dem ersten Buchstaben des Nachnamens:

Nachklausur

  • Termin: Samstag 4. Oktober 2014, 10-13 Uhr
  • Raum: Hörsaal B 001, Oettingenstr. 67
  • Einlass: ca. 10:00 Uhr
  • Beginn: 10:15 Uhr; Nach Beginn ist kein Einlass mehr möglich.
  • 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.
  • 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