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

Wintersemester 2017/2018

Formale Systeme

Prof. Dr. Bernhard Beckert (BB)
Dr. Mattias Ulbrich, Mihai Herda

Die Ergebnisse der Nachklausur sind jetzt verfügbar.
Die Klausureinsicht findet am Donnerstag 18.10.2018, 11:00 Uhr im Raum 201 (Geb. 50.34) statt.
Die Musterlösung zur Nachklausur ist hier verfügbar.

Typ: Vorlesung
Zielgruppe: Bachelor Informatik, Master Informatik
Umfang: 4 SWS / 6 Leistungspunkte
Ort: Gaede-Hörsaal (Geb. 30.22)
Zeit: Donnerstag, 14:00-15:30 Uhr
Freitag, 11:30-13:00 Uhr

Aktuelles

  • 26.02.18: Informationen zur Klausur am 28.02.2018 sind jetzt verfügbar.
  • 23.02.18: Die Bonuspunkte aus diesem Semester sind jetzt verfügbar.
  • 22.02.18: Altklausuren aus den letzten drei Jahren mit Musterlösung sind jetzt verfügbar.
  • 19.02.18: Foliensatz für Tableau, der in der Vorlesung verwendet wurde, ist jetzt online.
  • 07.02.18: Die Ergebnisse vom zweiten Zwischentest sind jetzt online.
  • 20.12.17: Die Ergebnisse vom ersten Zwischentest sind jetzt online.
  • 26.09.17: ILIAS Kurs ist jetzt online.

Materialien

Skriptum

skriptum.pdf

Aufgabensammlung

aufgaben.pdf (08.02.2016)
loesungen.pdf (08.02.2016)

Übungsaufgaben


Folgende Aufgaben werden/wurden besprochen:
  • Einleitende Beispiele: Aufgabe 2
  • Interpolaten: Aufgaben 8, 9
  • Normalformen: Aufgaben 11, 12, 13
  • Shannongraphen: Aufgaben 20, 21, 22
  • DPLL: Aufgabe 28
  • Substitutionen: Aufgaben 30, 31, 34
  • Semantik der Prädikatenlogik: Aufgaben 39, 43, 44
  • Normalformen (PL1): Aufgaben 47, 48

Forum und Einreichung von Lösungen der Praxisaufgaben

Bitte beachten Sie die Regeln. Insbesondere dürfen keine Lösungen gepostet werden.


Folien


Organisatorisches: bildschirm - druck

Syntax und Semantik der Aussagenlogik: bildschirm - druck

Craigsches Interpolationslemma: bildschirm - druck

Kurze Konjunktive Normalform: bildschirm - druck

Shannon-Graphen, OBBDs: bildschirm - druck

Das Erfüllbarkeitsproblem der Aussagenlogik, DPLL-Verfahren: bildschirm - druck

Einführung in die Prädikatenlogik: bildschirm - druck

Semantik der Prädikatenlogik: bildschirm - druck

Normalformen für Formeln der Prädikatenlogik: bildschirm - druck

Beweistheorie - Einführendes Beispiel: bildschirm - druck

Hilbertkalkül: bildschirm - druck

Resolutionskalkül für die Aussagenlogik: bildschirm - druck

Resolutionskalkül für die Prädikatenlogik: bildschirm - druck

Tableaukalkül für die Aussagenlogik: bildschirm - druck

Tableaukalkül für die Prädikatenlogik: bildschirm - druck

Tableaukalkül: bildschirm - druck

Sequenzenkalkül: bildschirm - druck

Peano-Arithmetik: bildschirm - druck

Java Modeling Language: bildschirm
(JML Homepage, JML Reference Manual, Theorembeweiser KeY)

Reduktionssysteme: bildschirm - druck

Termersetzungssysteme: bildschirm - druck

Modallogik: bildschirm - druck

Lineare Temporale Logik (LTL): bildschirm - druck

Büchi-Automaten: bildschirm - druck

LTL und Büchi-Automaten: bildschirm - druck

LTL und Model Checking: bildschirm - druck


Wiederholung: bildschirm - druck

Praxisaufgaben

Sie können Ihre Lösungen zu Praxisaufgaben einreichen, um Bonuspunkte für den Übungsschein zu erzielen (s.u.).
Die Abgabe erfolgt im ILIAS-Modul zur Vorlesung.


Ausgabe am
 Abgabe bis
praxis1.pdf 16.11.2017 07.01.2018 Benötigte Dateien: 1.0

1.1 (January 04, 2018)

  • [FIX] MyNonogramSolver Template compiles now.
  • [NEW] Runner without threading. On my system the java process takes up to 140 - 160 %. Maybe spin waiting on Thread#join() FastRunner does not use Threads, but does not offer timeout.
  • [FIX] Error in solution handling, missing.
  • [NEW] Add Java sources to the jar file.
praxis2.pdf 26.01.2018 21.02.2018 Benötigte Dateien: Count.java

Link zur Webseite des vorigen Jahres