Halbmodul Model Checking

Die Veranstaltung ist ein Halbmodul (es werden 5 bzw. 7,5 CP vergeben) für den Masterstudiengang im Bereich praktische oder theoretische Informatik.

Es sollen Grundlage des Model Checkings vermittelt werden. Dazu setzen wir auf eine umfangreiche Praxisphase, in der die Studierenden selbstständig einen Model Checker für eine vorgegebene Sprache entwickeln. So können die theoretischen Inhalte der Veranstaltung sofort eingeübt werden.

Die Veranstaltung basiert auf dem Praxisprojekt und kombiniert es mit theoretischem Input. Wir werden während des Semesters immer wieder die Anbindung an aktuelle Forschung aus dem Bereich suchen.

Genaue Inhalte und das Veranstaltungsformat sollen beim ersten Termin mit den Teilnehmern abgesprochen werden.

Dieser Kurs ist geeignet für Studierenden des Masterstudiengangs der Informatik. Da der Kurs auf den Bereich der theoretischen Informatik entfällt, wird dieser sowohl als praktisches als auch als theoretisches Schwerpunkt- oder Wahlpflichtmodul angeboten. Als Voraussetzungen für den Kurs werden folgende Kenntnisse erwartet:

• Automatentheorie
• Algorithmen und Datenstrukturen
• Mathematische Logik
• Programmierkenntnisse (in Java)

Die Materialien zur Vorlesung werden über ILIAS verteilt. Sie können sich mit Ihrer Universitätskennung einloggen. Sollten Sie wider Erwarten keinen Zugriff haben, melden Sie sich bitte per Mail bei Philipp Körner oder Joshua Schmidt.

• Vorlesung: Mi. 12:30 - 14:00 Uhr in Raum 25.12.02.55
  • Theoretische Inhalte, Model Checking Algorithmen
• Übung: Fr. 12:30 - 14:00 Uhr in Raum 25.12.02.55
  • Besprechung der Übungsblätter
• Klausur: Mittwoch den 18.07.2018, 12:30 Uhr - 14:00 Uhr, HS 5F (der letzte Vorlesungstermin)

• Christel Baier und Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008.
• Clarke, Grumberg, Peled: Model Checking. MIT Press, 1999.
• Michael Leuschel und Michael Butler: ProB: An Automated Analysis Toolset for the B Method. STTT, 2008.
• Daniel Plagge und Michael Leuschel: Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more. STTT, 2007.
• Steve Schneider: The B Method, PALGRAVE MACMILLAN, 2001.