Ausgewählte Themen aus dem Gebiet der Formalen Methoden der Softwareentwicklung werden in der Vorlesung vorgestellt und in der Übung vertieft. Der mathematische Hintergrund der vorgestellten Methoden wird behandelt und ihre praktische Anwendung wird anhand prototypischer Beispiele diskutiert. Mögliche Themen sind u. a.: Petrinetze und ihre Analyse, Methoden zur formalen Spezifikation des funktionalen Verhaltens, Programmverifikation, Programmanalyse, Semantik von Programmiersprachen, automatisches Theorembeweisen.
- Lehrende/r: Sebastian Kenter
- Lehrende/r: Markus Müller-Olm
Eine zunehmend auch von der Industrie eingesetzte Technik zur Aufdeckung versteckter Fehler in Hard- und Softwaresystemen ist das sogenannte Model-Checking. Ein Model Checker überprüft automatisch, ob ein Modell eines Systems eine gewünschte, typischerweise in einer temporalen Logik spezifizierte Eigenschaft besitzt. Die Vorlesung behandelt die verschiedenen Ansätze zur Konstruktion von Model-Checkern sowie theoretische und praktische Fragestellungen im Umfeld dieser Methode.
- Lehrende/r: Sebastian Kenter
- Lehrende/r: Markus Müller-Olm