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 2016/2017

Formale Systeme

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

Informationen zur Nachklausur.

Typ: Vorlesung
Zielgruppe: Diplom Informatik, 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.06.17 Die Nachklausur steht jetzt fest
  • 01.03.17 Informationen zur Klausur.
  • 08.02.17 Aufgaben zu Modallogik und LTL hinzugefügt.
  • 06.02.17 Ergebnisse vom zweiten Zwischentest sind jetzt online
  • 30.01.17 Aufgaben zu Sequenzenkankül, JML und Reduktionssysteme hinzugefügt.
  • 23.01.17 Aufgaben zum prädikatenlogischen Tableaukalkül hinzugefügt.
  • 22.12.16 Aufgaben zum prädikatenlogischen Resolutionskalkül hinzugefügt.
  • 16.12.16 Aufgaben zum Hilbert- und aussagenlogichen Resolutionskalkül sowie Lösungen zur Prädikatenlogik hinzugefügt.
  • 16.12.16 Ergebnisse vom ersten Zwischentest sind jetzt online
  • 25.11.16 Aufgaben zur Prädikatenlogik und Lösungen zur Aussagenlogik hinzugefügt.
  • 18.11.16 Hausaufgaben aktualisiert
  • 14.11.16 Aufgaben zur Aussagenlogik hochgeladen.
  • 20.10.16: Die Vorlesung am Freitag 21.10.2016 fällt aus.
  • 20.10.16: Terminliste veröffentlicht.
  • 07.10.16: ILIAS Kurs ist jetzt online

Materialien

Skriptum

skriptum.pdf

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

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

Endliche Automaten - kurze Wiederholung: bildschirm - druck

Büchi-Automaten: bildschirm - druck

Lineare Temporale Logik (LTL): bildschirm - druck

LTL und Büchi-Automaten: bildschirm - druck

LTL und Model Checking: bildschirm - druck


Wiederholung: bildschirm - druck


Aufgabensammlung

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

Hausaufgaben


Folgende Aufgaben wurden als Hausaufgabe gegeben:
  • 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

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 27.11.2016 08.01.2017 Benötigte Dateien: 1.0 1.1

1.1: Performance-Verbesserungen bei Lösungsüberprüfung, Änderungen bei der Zeitmessung
praxis2.pdf 01.02.2017 01.03.2017 Benötigte Dateien: InsertionSort.java

Übungsschein

Im Laufe des Semesters finden zwei Zwischentests statt und es gibt zwei Praxisaufgaben (s.o.). Die Teilnahme an den Zwischentests und den Praxisaufgaben ist freiwillig. Die erzielten Übungspunkte werden mit den erzielten Punkten der bestandenen Abschlussklausur verrechnet.


Abschlussklausur

Termine

Donnerstags findet immer eine Vorlesung statt, freitags Vorlesung oder Übung.

  • Do 20.10.2016
  • Do 27.10.2016
  • Fr 28.10.2016
  • Do 03.11.2016
  • Fr 04.11.2016
  • Do 10.11.2016
  • Fr 11.11.2016
  • Do 17.11.2016
  • Fr 18.11.2016
  • Do 24.11.2016
  • Fr 25.11.2016
  • Do 01.12.2016
  • Fr 02.12.2016
  • Do 08.12.2016
  • Fr 09.12.2016
  • Do 15.12.2016
  • Fr 16.12.2016
  • Do 22.12.2016
  • Fr 23.12.2016
  • Do 12.01.2016
  • Fr 13.01.2016
  • Do 19.01.2016
  • Fr 20.01.2016
  • Do 26.01.2016
  • Fr 27.01.2016
  • Do 02.02.2016
  • Fr 03.02.2016
  • Do 09.02.2016
  • Fr 10.02.2016

Inhaltsübersicht

  • Aussagenlogik
    • Syntax und Semantik
    • Kalküle
    • Anwendungen
  • Prädikatenlogik
    • Syntax und Semantik
    • Kalküle
    • Anwendungen
  • Gleichheit
  • Java Modeling Language (JML)
  • Modale Aussagenlogik
  • Temporale Logik (LTL)
  • Endliche Automaten (Wiederholung)
  • Büchi Automaten
  • Modellprüfung

Link zur Webseite des vorigen Jahres