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

Wahlpflichtvorlesung/Stammmodul im Wintersemester 2009/2010

Prof. Dr. Bernhard Beckert, Dr. Vladimir Klebanov

Aktuelles

13.05.10: Vorläufige Ergebnisse der Klausur vom 08.04.10 sind verfügbar. Die Klausureinsicht findet am Montag, dem 31.05.10, 13:00 Uhr, im Raum 201 statt.
06.04.10: Hörsaalverteilung für die Klausur am 08.04.: Alle Teilnehmer schreiben im HSaF.
10.03.10: Vorläufige Ergebnisse der Hauptklausur sind online. Die Klausureinsicht findet am Donnerstag, dem 11.03.10 ab 14:00 Uhr in zwei Gruppen im Raum SR236 statt: Die Teilnehmer aus dem Gerthsen HS ab 14:00 Uhr und die Teilnehmer aus dem HSaF ab 15:00 Uhr.
02.03.10: Die Anmeldung zur Nachklausur ist bis zum 01.04. im Studierendenportal des KIT möglich.
22.02.10: Die Klausureinsicht zur Klausur "Formale Systeme" am 18.02.10 findet am Donnerstag, dem 11.03.10, 14:00 Uhr, in SR236 statt.
21.02.10: Die Klausureinsicht zur Klausur "Formale Systeme" am 18.02.10 findet am Donnerstag, dem 11.03.10, 14:00 Uhr, statt. Der Raum wird noch bekannt gegeben.
17.02.10: Hörsaalverteilung für die Klausur am 18.02.: nach dem ersten Buchstaben des Nachnamens: A-O im Gerthsen HS, P-Z im HSaF.
15.02.10: Die vorläufige (!) Bewertung der 1. Praxisaufgabe steht im LOGIN Bereich zur Verfügung. Details zur Auswertung.
12.02.10: Die Lösungen zum 12. Übungsblatt stehen zur Verfügung.
12.02.10: Die Folien zu den Vorlesungen am 11.02.10 und 12.02.10 stehen zur Verfügung.
10.02.10: Die Ergebnisse des 2. Zwischentests stehen ab sofort im LOGIN Bereich zur Verfügung. Die Einsicht in beide Zwischentests findet am Donnerstag, dem 11.02.10, um 16 Uhr (Gruppe 1) bzw. 17 Uhr (Gruppe 2) in SR236 statt. Gruppe 1: alle, die bei dem ersten Zwischentest in der 1. Gruppe mitgeschrieben haben; Gruppe 2: alle anderen.
08.02.10: Das 12. Übungsblatt steht zur Verfügung. Es wird am 12.02.10 besprochen.
07.02.10: Die Folien zur Vorlesung am 04.02.10 stehen zur Verfügung
07.02.10: Die Lösungen zum 10. Übungsblatt und zum 11. Übungsblatt stehen zur Verfügung. In der Übung am 05.02. wurden (neben der Musterlösung zum 2. Zwischentest) nur die Lösungen zum 10. Übungsblatt besprochen. Die Lösungen zum 11. Übungsblatt werden am 12.02. besprochen.
06.02.10: Erratum: Die Musterlösung zu Aufgabe 3 b iii des 5. Übungsblatts war fehlerhaft. Sie ist nun korrigiert.
01.02.10: Das 11. Übungsblatt steht zur Verfügung. Es wird in der übung am 05.02.10 besprochen.
01.02.10: Die Anmeldung zur Hauptklausur ist ab sofort im Studierendenportal des KIT möglich.
29.01.10: Die Aufgaben und die Musterlösung zum 2. Zwischentest am 28.01. stehen zur Verfügung.
28.01.10: Mit der Anmeldung zur Hauptklausur gibt es noch ein technisches Problem. Wir arbeiten daran.
28.01.10: Ein wenig Statistik zum 1. Zwischentest:
Ab 15 Verrechnungspunkten gab es 0,5 Bonuspunkte und ab 27 Verrechnungspunkten 3,0 Bonuspunkte (ansonsten besteht eine lineare Abhängigkeit).
Es gab 178 Teilnehmer.
Der Mittelwert der Verrechnungspunkte war 22,7; der Mittelwert der erreichten Bonuspunkte war 1,9.
Die Verteilung war: 13x 0,0 - 12x 0,5 - 24x 1,0 - 23x 1,5 - 28x 2,0 - 29x 2,5 - 49x 3,0.
Die maximale Zahl von 30 Verrechnungspunkten erzielten 7 Teilnehmer.
27.01.10: Die Einteilung der Gruppen und Sitzplätze für den 2. Zwischentest steht zur Verfügung. Beachten Sie bitte auch die Hinweise zum Ablauf.
27.01.10: Die Einsicht in beide Zwischentests findet am Donnerstag, dem 11.02.10, um 16 Uhr (Gruppe 1) bzw. 17 Uhr (Gruppe 2) in SR236 statt. Gruppe 1: alle, die bei dem ersten Zwischentest in der 1. Gruppe mitgeschrieben haben; Gruppe 2: alle anderen.
27.01.10: Die Ergebnisse des 1. Zwischentests stehen ab sofort im LOGIN Bereich zur Verfügung.
25.01.10: Das 10. Übungsblatt steht zur Verfügung. Es wird in der Übung am 05.02.10 besprochen.
22.01.10: Die Lösungen zum 8. und 9. Übungsblatt stehen zur Verfügung.
22.01.10: Die Folien zur Vorlesung am 21.01.10 stehen zur Verfügung
19.01.10: Das 9. Übungsblatt steht zur Verfügung. Es wird in der Übung am 22.01.10 besprochen.
16.01.10: Korrektur: Die Musterlösung zu Aufgabe 2 (e) auf Blatt 6 war fehlerhaft, weil die in der Lösung verwendete Formel eine andere war als die auf dem Aufgabenblatt. Dies ist nun korrigiert.
15.01.10: Die Folien zu den Vorlesungen am 14.01. und 15.01. stehen zur Verfügung.
11.01.10: Das 8. Übungsblattes steht zur Verfügung. Es wird zusammen mit den restlichen Aufgaben des 7. Übungsblattes in der Übung am 22.01.10 besprochen.
11.01.10: Korrektur: Im Aufgabenblatt für die 2. Praxisaufgabe war ein Fehler in der Axiomatisierung von count. Dieser ist nun korrigiert. In der Formalisierung in der Datei inssort.key trat der Fehler nicht auf.
11.01.10: Ein Java-Applet zum Visualisieren des Tableau-Kalküls steht zur Verfügung.
10.01.10: Die Lösungen zum 7. Übungsblatt stehen zur Verfügung. In der Übung am 08.01. wurden die Lösungen zu den restlichen Aufgaben des 6. Blatt und Aufgabe 1 (a) 7. Blattes besprochen. Die restlichen Aufgaben des 7. Blattes werden in der nächsten Übung besprochen.
10.01.10: Die Folien zur Vorlesung am 07.01. stehen zur Verfügung.
08.01.10: Die 2. Praxisaufgabe steht zur Verfügung. Die Lösung kann bis zum 14.02. abgegeben werden.
04.01.10: Die Anmeldung zum 2. Zwischentest ist freigeschaltet: LOGIN. Die Anmeldung ist möglich bis zum 24.01.10 (bis dahin kann man sich auch wieder abmelden).
22.12.09: Das 7. Übungsblattes steht zur Verfügung. Es wird zusammen mit den restlichen Aufgaben des 6. Übungsblatt in der Übung am 08.01.10 besprochen.
20.12.09: Die Folien zu den Vorlesungen am 17. und 18.12. stehen zur Verfügung.
15.12.09: Die Musterlösung zum 1. Zwischentest am 9.12. steht zur Verfügung.
15.12.09: Die Lösungen zum 5. und 6. Übungsblatt stehen zur Verfügung. In der Übung am 10.12. wurde die Lösung zum 5. Blatt und die erste Aufgabe des 6. Blattes besprochen. Die restlichen Aufgaben des 6. Blattes werden in der nächsten Übung besprochen.
10.12.09: Die Einteilung der Gruppen und Sitzplätze für den 1. Zwischentest steht zur Verfügung.
07.12.09: Das 6. Übungsblatt steht zur Verfügung. Es wird zusammen mit dem 5. Übungsblatt in der Übung am 11.12.09 besprochen.
04.12.09: Die Folien zur gestrigen und zur heutigen Vorlesung stehen zur Verfügung.
02.12.09: Stoff des 1. Zwischentests ist der Inhalt der Vorlesungen bis einschließlich 20.11.09, also bis einschließlich der Definition von Substitutionen aber ohne Unifikation.
29.11.09: Das 5. Übungsblatt steht zur Verfügung. Es wird zusammen mit dem 6. Übungsblatt in der Übung am 11.12.09 besprochen.
28.11.09: Letzte Woche erschien in der Frankfurter Allgemeinen Sonntagszeitung ein interessanter Artikel über Leben und Werk Gerhard Gentzens, des "Erfinders" des Sequenzenkalküls. Am Ende des Artikels wird auch die Bedeutung der Sequenzen in der heutigen Informatik erwähnt, insbesondere als Werkzeug für die Programmverifikation (das wird Thema der zweiten Praxisaufgabe sein).
27.11.09: Die Webseite zur Anmeldung zu den Zwischentests und zur Abgabe der Lösung der Praxisaufgaben ist freigeschaltet: LOGIN (beim ersten Login Registrierung mit der Matrikelnummer). Die Anmeldung zum 1. Zwischentest ist möglich bis zum 06.12.09 (bis dahin kann man sich auch wieder abmelden). Die Lösung zur 1. Praxisaufgabe kann bis zum 03.01.10 abgegeben werden.
27.11.09: Die Lösungen zum 3. und 4. Übungsblatt, wie heute in der Übung besprochen, stehen zur Verfügung.
27.11.09: Die Folien zur gestrigen Vorlesung stehen zur Verfügung.
25.11.09: Update des Sat-o-ban Rahmenwerks (v1.0.1): Off-by-one-Fehler in den Methoden fü die AL-Variablen in Solver.java behoben.
24.11.09: Die erste Praxisaufgabe steht zur Verfügung. Die Lösung kann bis zum 03.01.10 abgegeben werden. Die Webseite dafür wird bald freigeschaltet.
23.11.09: Das 4. Übungsblatt steht zur Verfügung. Es wird in der Übung am 27.11.09 besprochen.
21.11.09: Die Folien zu den Vorlesungen am 19.11. und 20.11. stehen zur Verfügung.
16.11.09: Das 3. Übungsblatt steht zur Verfügung. Es wird zusammen mit dem 4. Übungsblatt in der Übung am 27.11.09 besprochen.
14.11.09: Die Lösung zum 2. Übungsblatt steht zur Verfügung. (Die Folien zur Vorlesung am 12.11.09 waren schon online.)
09.11.09: Das 2. Übungsblatt steht zur Verfügung. Es wird in der Übung am 13.11.09 besprochen.
06.11.09: Die Folien zur gestrigen und zur heutigen Vorlesung stehen zur Verfügung.
30.10.09: Korrigierte Version der Lösung zum 1. Übungsblatt (in der Definition von Diag+ und Diag- in der Lösung zu Aufgabe 1 fehlte eine Bedingung).
30.10.09: Die Lösung zum 1. Übungsblatt steht zur Verfügung.
30.10.09: Die Folien zur gestrigen Vorlesung stehen zur Verfügung.
26.10.09: Das 1. Übungsblatt steht zur Verfügung. Es wird in der Übung am 30.10.09 besprochen.
23.10.09: Die Termine für die Abschlussklausuren sind Donnerstag, der 18.02.10 (Hauptklausur), und Donnerstag, der 08.04.10 (Nachklausur).
23.10.09: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
22.10.09: Die Folien zur heutigen Vorlesung stehen zur Verfügung.
21.10.09: Weitere organisatorische Informationen auf der Webseite.
01.10.09: Webseite angelegt.

Materialien

Vorlesungsfolien

Die Vorlesungsfolien werden hier jeweils nach der Vorlesung zur Verfügung gestellt.

  1. Organisatorisches: bildschirm - druck
    Vorlesung am 22.10.09
  2. Aussagenlogik, Syntax und Semantik: bildschirm - druck
    Vorlesung am 22.10.09
  3. Aussagenlogik, Normalformen: bildschirm - druck
    Vorlesung am 23.10.09
  4. Binary Decision Diagrams: bildschirm - druck
    Vorlesung am 23.10.09
  5. Aussagenlogik, Erfüllbarkeisproblem spezieller Formelklassen: bildschirm - druck
    Vorlesung am 29.10.09
  6. Hilbert-Kalkül: bildschirm - druck
    Vorlesung am 29.10.09 bis Folie 7, Vorlesung am 05.11.09 ab Folie 8
  7. Aussagenlogik, Resolution: bildschirm - druck
    Vorlesung am 05.11.09 bis Folie 9, Vorlesung am 06.11.09 ab Folie 10
  8. Aussagenlogik, Tableaukalkül: bildschirm - druck
    Vorlesung am 06.11.09 bis Folie 9, Vorlesung am 12.11.09 ab Folie 10
  9. Aussagenlogik, Sequenzenkalkül: bildschirm - druck
    Vorlesung am 19.11.09
  10. Aussagenlogik, sonstige Kalküle: bildschirm - druck
    Vorlesung am 19.11.09
  11. Prädikatenlogik, Syntax: bildschirm - druck
    Vorlesung am 20.11.09 bis Folie 19, Vorlesung am 26.11.09 ab Folie 20
  12. Prädikatenlogik, Semantik: bildschirm - druck
    Vorlesung am 03.12.09 bis Folie 39, Vorlesung am 04.12.09 ab Folie 40
  13. Prädikatenlogik, Normalformen: bildschirm - druck
    Vorlesung am 04.12.09
  14. Prädikatenlogik, Resolution: bildschirm - druck
    Vorlesung am 17.12.09
  15. Prädikatenlogik, Tableaukalkül: bildschirm - druck
    Vorlesung am 18.12.09 (Folien 1 bis 14 und Folien 37 und 38), Vorlesung am 07.01.10 (Folien 15 bis 36)
  16. Prädikatenlogik, Sequenzenkalkül: bildschirm - druck
    Vorlesung am 07.01.10
  17. Reduktionssysteme: bildschirm - druck
    Vorlesung am 14.01.10
  18. Termersetzung: bildschirm - druck
    Vorlesung am 14.01.10
  19. Prädikatenlogik 2. Stufe: bildschirm - druck
    Vorlesung am 15.01.10
  20. Modallogik: bildschirm - druck
    Vorlesung am 15.01.10 (Folien 1 bis 22), Vorlesung am 21.01.10 (Folien 23 bis 39)
  21. Object Contraint Language: bildschirm - druck
    Vorlesung am 21.01.10 (Folien 1 bis 17), Vorlesung am 29.01.10 (Folien 18 bis 42)
  22. Endliche Automaten (Wiederholung): bildschirm - druck
    Vorlesung am 04.02.10 (kurze Wiederholung an der Tafel ohne Folien)
  23. Büchi-Automaten: bildschirm - druck
    Vorlesung am 04.02.10
  24. Die Beschreibungssprache PROMELA für Büchi-Automaten: bildschirm - druck
    Vorlesung am 11.02.10
  25. Lineare Temporale Logik (LTL): bildschirm - druck
    Vorlesung am 11.02.10
  26. LTL, Übersetzung in Büchi-Automaten: bildschirm - druck
    Vorlesung am 11.02.10 (Folien 1 bis 6), Vorlesung am 12.02.10 (Folien 7 bis 14)
  27. LTL, Model Checking: bildschirm - druck
    Vorlesung am 12.02.10

Übungsblätter

Alle zwei Wochen wird hier ein Übungsblatt bereitgestellt, und zwar immer am Montag derjenigen Wochen, in denen am Freitag eine Übung stattfindet. Die Lösungen werden dann in der Übung am Freitag besprochen.

Übungsblatt
 Ausgabe am
 Besprechung am
 Lösung
blatt1.pdf 26.10.09 30.10.09 loesung1.pdf
blatt2.pdf 09.11.09 13.11.09 loesung2.pdf
blatt3.pdf 16.11.09 27.11.09 loesung3.pdf
blatt4.pdf 23.11.09 27.11.09 loesung4.pdf
blatt5.pdf 29.11.09 11.12.09 loesung5.pdf
blatt6.pdf 07.12.09 11.12.09 / 08.01.10 loesung6.pdf
blatt7.pdf 22.12.09 08.01.10 / 22.01.10 loesung7.pdf
blatt8.pdf 11.01.10 22.01.10 loesung8.pdf
blatt9.pdf 19.01.10 22.01.10 loesung9.pdf
blatt10.pdf 25.01.10 05.02.10 loesung10.pdf
blatt11.pdf 01.02.10 05.02.10 loesung11.pdf
blatt12.pdf 08.02.10 12.02.10 loesung12.pdf

Die Lösungen müssen nicht abgegeben werden. Das birgt die Gefahr in sich, dass man sich nicht hinreichend mit den Aufgaben beschäftigt, sondern im schlimmsten Falle lediglich in der nächsten Übung die Lösungen unverstanden abschreibt. Das führt nicht zum Erfolg! Bitte lösen Sie die Aufgaben selbständig, am besten in kleinen(!) Lerngruppen von zwei, allenfalls drei Teilnehmern. So sind Sie für die Klausuren gut vorbereitet.

Newsgroup

In der Newsgroup uka.formsys

  • werden Ankündigungen und Informationen zu Vorlesung und Übung gepostet,
  • können inhaltliche Fragen gestellt werden, die dann in der Newsgroup beantwortet werden.

Skriptum

  • skriptum.pdf (in der Version des WS 07/08, diese kann sich im Laufe des Semesters geringfügig ändern)

Tableau-Applet

Praxisaufgaben

Im Laufe des Semesters werden zwei Praxisaufgaben mit längerer Bearbeitungszeit angeboten. Ihre Bearbeitung gibt Ihnen Gelegenheit, sich mit Implementierungen formaler Verfahren vertraut zu machen.

Aufgabenstellung
 Ausgabe am
 Abgabe bis zum
 Bemerkungen
praxis1.pdf / satobanSrc-1.0.1.zip / minisat2-070721.zip 24.11.09 03.01.10 Abgabe: LOGIN.
praxis2.pdf / inssort.key / KeYIntro.pdf 03.01.10 14.02.10

Die Bearbeitung der Praxisaufgaben ist freiwillig. Jedoch können und sollen Sie Ihre Lösungen zu den Praxisaufgaben abgeben. Für die erfolgreiche Bearbeitung der beiden Praxisaufgaben werden jeweils bis zu 1,5 Bonuspunkte vergeben (s.u.).

Erfolgskontrolle und Notenvergabe

Abschlussklausur

Die Endnote (Modulnote) ist die Note der Abschlussklausur unter Berücksichtigung der für die Zwischentests und Praxisaufgaben vergebenen Bonuspunkte (s.u.).

Die 1. Abschlussklausur (Hauptklausur) findet am Donnerstag, dem 18.02.10, 9:00 Uhr, statt (Gerthsen, HSaF, Daimler, HS37).
Die 2. Abschlussklausur (Nachklausur) findet am Donnerstag, dem 08.04.2010, 9:00 Uhr, statt (Gerthsen, HSaF).

Zur Hauptklausur kann man sich vom 19.01.10 bis zum 15.02.10 anmelden; zur Nachklausur vom 01.03.10 bis zum 01.04.10. Die Anmeldung ist im Studierendenportal des KIT möglich.

Aufgaben und Musterlösungen

Abschlussklausur
am
 Aufgabenstellung
 Musterlösung
18.02.10 Aufgaben Lösungen
08.04.10 Aufgaben Lösungen

Zwischentests ("Zwischenklausuren")

Im Laufe des Semesters werden zwei Zwischentests angeboten. Die Teilnahme daran ist freiwillig. Bei erfolgreicher Teilnahme werden pro Zwischentest bis zu drei Bonuspunkte für die Abschlussklausur vergeben (s.u.).

Der 1. Zwischentest findet am Donnerstag, dem 10.12.09, um 14:00 statt; der 2. Zwischentest am Donnerstag, dem 28.01.10, um 14:00. Die Anmeldung zum ersten Test erfolgt vom 24.11.09 bis 06.12.09 über diese Webseite; die Anmeldung zum zweiten Test vom 01.01.10 bis zum 24.01.10.

An-/Abmeldung zu Zwischentests hier: LOGIN.

Aufgaben und Musterlösungen

Zwischentest
am
 Aufgabenstellung
 Musterlösung
10.12.09 Aufgaben Lösungen
28.01.10 Aufgaben Lösungen

Bonuspunkte

Für die erfolgreiche Teilnahme an den beiden Zwischentests werden jeweils bis zu drei Bonuspunkte und für die erfolgreiche Bearbeitung der beiden Praxisaufgaben jeweils bis zu 1,5 Bonuspunkte vergeben.

Diese Bonuspunkte werden bei der Abschlussklausur zur Notenverbesserung angerechnet. Sie können allerdings nur zur Notenverbesserung eingesetzt werden, wenn die Abschlussklausur auch ohne sie schon bestanden wäre. Das heißt, es ist nicht möglich, eine nicht bestandene Abschlussklausur mit Hilfe der Bonuspunkte zu bestehen.

Termine

Vorlesung/Übung

  • Donnerstags, 14:00 - 15:30 Uhr, Gaede-Hörsaal (Geb. 30.22, Raum 130.1)
  • Freitags, 11:30 - 13:00 Uhr, Gaede-Hörsaal (Geb. 30.22, Raum 130.1)

Abschlussklausuren

  • Anmeldung zur 1. Abschlussklausur: 19.01.10 bis 15.02.10
  • 1. Abschlussklausur (Hauptklausur): Donnerstag, 18.02.2010, 9:00 Uhr, Gerthsen/HSaF/Daimler/HS37
  • Einsicht 1. Abschlussklausur: Donnerstag, 11.03.10, 14:00 Uhr, SR236 (Geb. 50.34)
  • Anmeldung zur 2. Abschlussklausur: 01.03.10 bis 01.04.10
  • 2. Abschlussklausur (Nachklausur): Donnerstag, 08.04.2010, 9:00 Uhr, Gerthsen/HSaF
  • Einsicht 2. Abschlussklausur: wird noch bekannt gegeben

Zwischentests

  • Anmeldung zum 1. Zwischentest: 24.11.09 bis 06.12.09 über diese Webseite
  • 1. Zwischentest: Donnerstag, 10.12.09, 14:00 Uhr, Gaede
  • Anmeldung zum 2. Zwischentest: 01.01.10 bis 24.01.10 über diese Webseite
  • 2. Zwischentest: Donnerstag, 28.01.10, 14:00 Uhr, Gaede
  • Einsicht: Donnerstag, 11.02.10, 16 Uhr (Gruppe 1) bzw. 17 Uhr (Gruppe 2), SR236
    Gruppe 1: alle, die bei dem ersten Zwischentest in der 1. Gruppe mitgeschrieben haben;
    Gruppe 2: alle anderen

An-/Abmeldung zu Zwischentests hier: LOGIN.

Praxisaufgaben

  • Abgabe der 1. Praxisaufgabe bis: 03.01.10
  • Abgabe der 2. Praxisaufgabe bis: 14.02.10

Inhaltsübersicht

  • Aussagenlogik
    • Syntax und Semantik
    • Kalküe
    • Anwendungen
  • Prädikatenlogik
    • Syntax und Semantik
    • Kalküle
    • Anwendungen
  • Gleichheit
  • Object Constraint Language (OCL)
  • Modale Aussagenlogik
  • Temporale Logik (LTL)
  • Endliche Automaten (Wiederholung)
  • Büchi Automaten
  • Modellprüfung

Link zur Webseite des vorigen Jahres