Modulnummer

Modulbezeichnung

Titel (englisch)

Pflicht/Wahl

Erklärung

CP

Berechnung des Workloads

Turnus

Dauer

Form

Prüfung

Anforderungen

Lernziele

Die Studierenden verfügen über:

• Vertiefte Kenntnisse in der Methodik formaler (logikbasierter) Systemspezifikation und -verifikation
• Verständnis von dafür verwendeten Beweis- und Analyseverfahren, insbesondere formaler Kalküle und ihrer Algorithmen
• Fähigkeit zur Verwendung formaler Modellierungs- und Verifikationswerkzeuge
• Fähigkeit zur Auswahl geeigneter Werkzeuge und Verfahren für praktische Fragestellungen

Lerninhalte

• Modellierung mit Logik erster und höherer Stufe, sowie sowie mit Temporallogiken
• Einführung in interaktive Modellierungswerkzeuge und Theorembeweiser
• Ausgewählte Beweisverfahren wie Modellprüfung (Modelchecking, Resolutionsbeweisen, Tableauverfahren)
• Semantik imperativer Sprachen und darauf basierende Verifikationskalküle

Quellen

Ausgewählte Texte aus folgenden:

• T. Nipkow, L. C. Paulson, M. Wenzel: Isabelle/HOL, a Proof Assistant for Higher-Order Logic. Springer 2002.
• M. R. Huth and M. D. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.
• G. Winskel: The formal semantics of programming languages, MIT Press, 1993.
• Edmund M. Clarke, Orna Grumberg and Doron Peled: Model Checking, MIT Press, 1999.
• D. van Dalen: Logik and Structure, Springer 2004.

Sowie Papiere und Handbücher auf der Webseite der Veranstaltung.

Sprache

Bemerkung

Zuletzt geändert