Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2015 / 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

  • Die Nachklausur findet am 30. September, 10-13 Uhr statt. Die Anmeldung bei UniWorx ist bis zum 22. September möglich.
  • Klausureinsicht: Donnerstag, 6. August, 17-18 Uhr, Raum L109, Oettingenstraße 67
  • Da die Donnerstagsübung am 4.6. wegen eines Feiertags entfällt, wird auch in der Übung am Mittwoch, den 3.6. kein neuer Stoff behandelt. Stattdessen kann der Übungstermin am Mittwoch, den 3.6. als Fragestunde genutzt werden. Zum Beispiel haben Sie die Gelegenheit, Hilfe bei der Lösung von Aufgabe 7-1 zu bekommen.
  • Raumänderung: Die Donnerstagsübung findet ab sofort im Raum U151 in der Oettingenstr. 67 statt.
  • Raumänderung: Die Mittwochsübung findet ab dem 6.5. im Raum 220 in der Amalienstr. 73a statt.
  • Der Klausurtermin steht jetzt fest. Bitte melden Sie sich bis zum 21. Juli bei Uniworx zur Klausur an.
  • Am 4.5. und 6.5. findet die Vorlesung nicht statt.
  • 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

Veranstaltung Zeit OrtBeginn
Vorlesung Mo, 12–14 c.t. Oettingenstr. 67, BU101 13.04.2015
Vorlesung Mi, 16–18 c.t. Oettingenstr. 67, BU101 15.04.2015
Übung Mi, 18–20 c.t. Amalienstr. 73a, Raum 220 22.04.2015
Übung Do, 10–12 c.t. Oettingenstr. 67, Raum U151 23.04.2015

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.DatumThemaDozentHinweise
1. 13.4. Organisation, Aussagenlogik: Syntax und Semantik, Modellierung von Sudoku. MH
2. 15.4. Aussagenlogik MH
3. 20.4 Aussagenlogik US Folien 36-56
4. 22.4. BDDs US Folien 57-72
5. 27.4. BDDs US Folien 73-83
6. 29.4. CTL, Model Checking US Folien 84-105
4.5.
6.5.
7. 11.5. Model-Checking-Algorithmen MH Folien 106-116 
8. 13.5. SMV, Fairness MH Folien 117-140
9. 18.5. Alternating Bit Protocol MH Folien 141-144
20.5.
25.5. (Pfingstmontag)
10. 27.5. Alternating Bit Protocol, Symbolic Model Checking MH Folien 145-149
11. 1.6. Zusammenfassung Kapitel 2; Programmanalyse: Motivation und Einführung MH
12. 3.6. Fixpunkttheorie MH
13. 8.6. Live Variablen, Einfache funktionale Sprache, einfaches Typsystem MH
10.6.
15.6.
14. 17.6. Typinferenz mit Algorithmus W und Unifikation MH
15. 22.6. Typ- und Effektsyteme: Exceptions und Referenzen MH
16. 24.6. Hoare Logik: Grundlagen US
17. 29.6. Hoare Logik: Methoden und Prozeduren US
18. 1.7. Spezifikation objektorientierter Programme: JML (Java Modelling Language) US
6.7.
8.7.
19. 13.7. Klausurwiederholung US

Materialien

Eine Übersicht über alle Materialien finden Sie hier.

Aufzeichnung der Vorlesung

Für Fragen zum Stoff gibt es ein Forum zu dieser Veranstaltung auf die-informatiker.net.


Übungen

 


Literatur


Klausur

Klausur

  • Termin: Di 28.07. 15-18 Uhr
  • Ort:
    • Hörsaal C 123, Theresienstr. 41: Nachnamen: A.–Scha.
    • Hörsaal B 004, Theresienstr. 39: Nachnamen: Schl.–Z. + Studenten mit Nachteilausgleich
  • Beginn: 15:15 Uhr; Nach Beginn ist kein Einlass mehr möglich.
  • Bearbeitungszeit: 120 Minuten

Nachklausur

  • Termin: Mi 30.09. 10-13 Uhr
  • Ort: Hörsaal B 001, Oettingenstr. 67
  • 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