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

Aktuelles

  • Der Klausurtermin wurde veröffentlicht
  • Die Veranstaltung findet ab sofort in S1|01 A01 statt
  • Der Link zum Moodle Kurs wurde hinzugefügt
  • Die Tutoren zu den jeweiligen Übungsgruppen sind nun verfügbar
  • Übungsgruppe F wird eingestellt; Gruppe D ab sofort in der Stadtmitte (siehe auch News im Moodle Kurs)
  • Raumzuteilung für die Klausur am 02. April 2015:
    x = Ihre Matrikelnummer
    • S206/030: x < 1906340
    • S101/A1: 1906340 <= x < 2373340
    • S311/08: 2373340 <= x < 2696840
    • S105/122: 2696840 <= x
  • Die Nachklausur findet am 22. September 2015 von 14:00 bis 16:00 Uhr statt
    • Alle Teilnehmer schreiben in Raum S1|01 A03
  • Die Einsicht der Nachklausur findet am 06.11.2015 von 16 bis 17 Uhr in Raum 4.3.01 (CASED) statt

Allgemeines

Form der Lehrveranstaltung: V2+Ü2
Veranstalter: Prof. Dr. Stefan Katzenbeisser, Christian Schlehuber
Zeit: Dienstag, 16:15 - 17:55 Uhr
Raum: S1|01 A01
Beginn: 13. Oktober 2014
Klausur: 02. April 2015, 11:30 - 13:30 Uhr

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 Christian Schlehuber. Die Übungen beginnen erst in der vierten Vorlesungswoche (d.h. beginnend ab dem 03.11.14).

  • Mittwoch, 09:00 – 10:30 (Raum S414|4.3.01 - CASED) (T: Christian Schlehuber)
  • Mittwoch, 09:50 – 11:30 (Raum S102|34) (T: Erich Wittenbeck)
  • Mittwoch, 11:40  13:20 (Raum S102|244) (T: Erich Wittenbeck)
  • Donnerstag, 08:00  09:40 (Raum S103|204) (T: Jan Erik Keller)
  • Donnerstag, 11:40 – 13:20 (Raum S103|12) (T: Jan Erik Keller)
  • Donnerstag, 14:25 – 16:05 (Raum S103|126) (T: Jan Erik Keller)
  • Freitag, 13:30 – 15:10 (Raum S103|126) (T: Nicolas Morew)
  • Freitag, 13:30 – 15:10 (Raum S414|3.1.01 - CASED) (T: Christian Schlehuber) 

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: https://moodle.informatik.tu-darmstadt.de/course/view.php?id=375

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: 7 days ago