Formale Grundlagen der Informatik 3 (V+Ü, 6 CP)

Aktuelles

  • 30. März 2017: Die Sprechstunde zur Nachklausur findet am Mi., dem 5.4.2017, von 13:30 bis 14:30 im Raum 4.3.01 im Gebäude S414 (4ter Stock, Eingang Fitnessstudio, Mornewegstr. 32) statt.
  • 16. März 2017: Die Nachkklausur im WS16/17 findet am 10.4.2017 in Raum S101/A1 (Audimax) von 9:30 bis 11:30 Uhr statt.
  • 15. März 2017: Nachkklausur im WS16/17 findet am 10.4.2017 statt. Die Klausur orientiert sich an der FGDI3 Vorlesung aus dem WS15/16, gehalten von Prof. Katzenbeisser. Ansprechpartner bzgl. der Klausur ist Dr. Sebastian Gabmeyer.

Allgemeines

Form der Lehrveranstaltung: V2+Ü2
Veranstalter: Prof. Dr. Stefan Katzenbeisser, Niklas Büscher
Zeit: Dienstag, 16:15 - 17:55 Uhr
Raum: S1|01 A01
Beginn: 13. Oktober 2015
Klausur: Mo, 4. Apr. 2016 11:30-13:30

Inhalte der Vorlesung

  • Modellierung nebenläufiger Software mit der Sprache ProMeLa
  • Formalisierung von Sicherheits- und Lebendigkeitseigenschaften mit temporaler Aussagenlogik 
  • theoretische Grundlagen von Modellprüfungsverfahren 
  • Verifikation von ProMeLa Programmen mittels des Modellprüfers SPIN 
  • Syntax, Semantik und Sequenzenkalkül für typisierte Logik erster Stufe 
  • Grundlagen der kontraktbasierten Softwarespezifikationssprache JML 
  • Dynamische Logik als eine Programmlogik erster Stufe 
  • Formale Programmverifikation durch symbolische Ausführung und Invariantenschließen 
  • Werkzeugunterstützte Verifikation von Java-Programen mit dem KeY System

Übungen

Verantwortlich für die Übungen ist Niklas Büscher. Die Organisation des Übungsbetriebs findet über den Moodle-Kurs statt.

  • Mittwoch, 09:50  11:30 (Raum S103|100) (T: Borhan Salem)
  • Mittwoch, 09:50  11:30 (Raum S115|020) (T: Nicolas Morew)
  • Mittwoch, 11:40 – 13:20 (Raum S101|A3) (T: Maximilian Mueller)
  • Mittwoch, 11:40 – 13:20 (Raum S320|5) (T: Daniel Guenther)
  • Donnerstag, 08:00  09:40 (Raum S103|204) (T: Philipp Becker)
  • Donnerstag, 08:00  09:40 (Raum S113|118) (T: Daniel Guenther)
  • Donnerstag, 11:40  13:20 (Raum S103|12) (T: Maximilian Mueller)
  • Donnerstag, 11:40  13:20 (Raum S115|138) (T: Veronika Schindler)
  • Donnerstag, 14:25  16:05 (Raum S422|5) (T: Maximilian Mueller)
  • Freitag, 13:30  15:10 (Raum S103|226) (T: Frederik Schwan)

Materialien

Sämtliche Materialien der Veranstaltung (Folien, Übungen, Hinweise zu Tools, etc.) werden über das Moodle zur Veranstaltung zur Verfügung gestellt.

Der Moodle-Kurs ist hier erreichbar: Moodle Kurs

Literaturhinweise

Ausgewählte Kapitel aus den folgenden Standardwerken:

  • Clarke, Grumberg and Peled, Model Checking, MIT Press, 1999

zum Seitenanfangzum Seitenanfang

A A A | Drucken Print | Impressum Impressum | Kontakt Contact | Last edited: 1 month ago