• Prof. Dr. Michael Elberfeld

• Prof. Dr. Michael Elberfeld
• Prof. Dr. Burkhardt Renz

Keine

Das Modul behandelt Grundkonzepte, Begriffe, Methoden und Werkzeuge, mit denen formale Methoden praktisch eingesetzt werden können, um sequentielle und nebenläufige Softwaresysteme zu modellieren und zu verifizieren.

• Grundlagen der Aussagenlogik: Sprache, Semantik, Natürliches Schließen, Normalformen, algorithmische Komplexität der Aussagenlogik, SAT-Solver
• Anwendungen der Aussagenlogik in der Softwaretechnik
• Grundlagen der Prädikatenlogik: Sprache, Semantik, Natürliches Schließen, Normalformen, Unentscheidbarkeit der Prädikatenlogik, Ausdruckskraft der Prädikatenlogik
• Anwendungen der Prädikatenlogik in der Softwaretechnik: Mikromodelle von Software Hoare-Kalküle

Fachkompetenzen

• Die Studierenden können grundlegende logische Konzepte und Begriffe erklären und einschätzen.

Methodenkompetenzen (fachlich & überfachlich)

• Die Studierenden können formale Methoden praktisch einsetzen bei der korrekten Modellierung sequenzieller und nebenläufiger Systeme.
• Sie können aus den erlernten Analysetechniken und Modellierungsansätzen diejenigen auswählen, welche geeignet sind, die für eine Anwendung interessierenden Systemeigenschaften anhand eines Modells zu verifizieren.

Sozialkompetenzen

• Die Studierenden können die Möglichkeiten und Grenzen der vorgestellten Ansätze und Werkzeuge im Team diskutieren.
• Sie können Andere von der Eignung eines gewählten Ansatzes zur Modellierung eines Systems überzeugen.

Selbstkompetenzen

• Die Studierenden können sich eigenständig neuere Entwicklungen zum Einsatz formaler Methoden erarbeiten und ihre Anwendbarkeit für eine gegebene Aufgabe einordnen.

• 6 CrP
• Arbeitsaufwand 180 Std.
• Präsenzzeit 60 Std.
• Selbststudium 120 Std.

• 4 SWS
• Vorlesung 2 SWS
• Übung 2 SWS

• Informatik (M.Sc. 2022)
• Ingenieur-Informatik (M.Sc. 2022)

Nein

Bonuspunkte werden gemäß § 9 (4) der Allgemeinen Bestimmungen vergeben. Art und Weise der Zusatzleistungen wird den Studierenden zu Veranstaltungsbeginn rechtzeitig und in geeigneter Art und Weise mitgeteilt.

Prüfungsvorleistung: Übungsaufgaben und/oder Hausübungen (Art und Anzahl wird den Studierenden rechtzeitig und in geeigneter Weise bekannt gegeben.)

Prüfungsleistung: Mündliche Prüfung oder Klausur (Art des Leistungsnachweises wird den Studierenden rechtzeitig und in geeigneter Weise bekannt gegeben.)

• Huth, M.; Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.
• Ben-Ari, M.: Mathematical Logic for Computer Science. Springer.
• Schenker, M.: Logikkalküle in der Informatik. Springer Vieweg.
• Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press.
• Renz, B.: lwb Logic WorkBench. https://github.com/esb-lwb/lwb/wiki.