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.

Kurs im HIS-LSF