Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Formale Systeme II: Theorie

Vorlesung im Sommersemester 2016

Prof. Dr. Bernhard Beckert (BB), Dr. Mattias Ulbrich (MU)

Zielgruppe: Master Informatik
Veranst.-Nummer: M-INFO-100841 / 24608
Umfang: 5 Leistungspunkte
Zeit: Dienstags, 11:30 Uhr
Freitags, 11:30 Uhr
Ort: R236, Geb. 50.34

Aktuelles

  • Am Dienstag, 07.06. findet keine Vorlesung statt.
  • Am Freitag, 25.06. findet keine Vorlesung statt.
  • Am Freitag, 8.7. findet keine Vorlesung statt.

Termine

Die Vorlesung ist dreistündig, also wird an einigen Terminen im Verlauf des Semesters keine Veranstaltung stattfinden.

An folgenden Terminen findet keine Vorlesung statt:

  • Freitag, 22. April
  • Freitag, 6. Mai (Brückentag)
  • Freitag, 27. Mai (Brückentag)
  • Dienstag, 7. Juni
  • Freitag, 25. Juni
  • Freitag, 8. Juli

Inhaltsübersicht

Geplant sind die folgenden Inhalte der Vorlesung:

  • Grundlagen der modalen/dynamischen Logik
    • Propositional Dynamic Logic (PDL)
    • Vollständigkeit der PDL
    • Relative Vollständigkeit der DL erster Stufe
    • Tableaukalküle
  • Separation Logic
  • Deduktive Verifikation hybrider Modelle
  • Axiomatische Mengenlehre nach Zermelo-Fraenkel
  • Mehrwertige Logik
  • Logik in der Sozialwahltheorie
  • ...

Es kann noch zu kurzfristigen Änderungen des Curriculums kommen.

 

Skript

Das Skript von Prof. Peter H. Schmitt deckt viel des Stoffes dieser Vorlesung ab. Wir werden das Skript an einigen wenigen Stellen noch erweitern, also wird sich die Version dieses Dokuments gelegentlich ändern:

Skript (Version vom 02.05.2016, 21:36 Uhr)

Ergänzende Literatur

Dynamische Logic:

  • D. Harel, D. Kozen, J. Tiury: Dynamic Logic (Foundations of Computing)
    MIT Press, 2000
    In der Fakultätsbibliothek vorhanden

Separation Logic

Termine

01.  VL am 19.04. Organisatorisches
Propositional Dynamic Logic (bis Dia 21, wird erweitert)
02. VL am 26.04. Propositional Dynamic Logic (bis Dia 43, wird erweitert)
03. VL am 29.04. Propositional Dynamic Logic (zu Ende)
First Order Dynamic Logic (bis Dia 22, wird erweitert)
04. VL am 03.05. First Order Dynamic Logic (zu Ende)
Übungsaufgaben
05. VL am 10.05. Logik in der Sozialwahltheorie: Teil A, Teil B, Teil C, Teil D
Wesentliche Teile dieser Folien stammen von Ulle Endriss (Universität von Amsterdam)
06. VL am 13.05. Logik in der Sozialwahltheorie (Forsetzung)
07. VL am 17.05. Logik in der Sozialwahltheorie (Fortsetzung)
08. VL am 20.05. Differentielle Dynamische Logik
Vorlesungsunterlagen von André Platzer an der CMU,
insbesondere Lecture Notes.
09. VL am 24.05. Differentielle Dynamische Logik: Differentielle Invarianten
Entscheidungsverfahren für semialgebraische Aussagen
10. VL am 31.05. Differentielle Dynamische Logik: Hybride Automaten, Übungen
11. VL am 03.06. Mehrwertige Logik
12. VL am 10.06. Mehrwertige Logik (Fortsetzung)
13. VL am 14.06. Mehrwertige Logik (Fortsetzung)
14. VL am 17.06. Separation Logic
15. VL am 21.06. Separation Logic (Fortsetzung)
16. VL am 28.06. Axiomatische Mengenlehre
17. VL am 01.07. Axiomatische Mengenlehre (Fortsetzung)
18. VL am 05.07. SAT und Phase Transition
Die Folien stammen von Carsten Sinz, KIT
19. VL am 12.07. Implementierung von Beweissuche in Prolog: Folien Vergleich Suchstrategien
Prolog-Programme dazu: search.pl, resolution.pl (zur Ausführung der Programme kann beispielsweise SWI Prolog verwendet werden)
20. VL am 15.07. Implementierung von Beweissuche in Prolog: Folien zum Tableaubeweiser leanTAP
Prolog-Programme dazu: leantap.pl, leantest.pl, nnf.pl, unify.pl (zur Ausführung der Programme kann beispielsweise SWI Prolog verwendet werden)
21. VL am 19.07. Description Logic
Die Folien stammen von Ulle Endriss (Universität von Amsterdam)

Prüfung

Mündlich nach Rücksprache mit den Dozierenden.