Verifizierte Model Checker

• Antragsteller: Professor Jan Kretinsky, Ph.D.; Dr. Peter Lammich
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2016 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 317422601

Model Checking ist die in der Praxis wichtigste Methode zur Verifikation von Hardware- und Softwaresystemen, d.h., zur Sicherstellung der Zuverlässigkeit dieser Systeme. Ziel des Projekts ist es, zwei unterschiedlich ausgerichtete Model Checker zu entwickeln und deren Korrektheit mit Hilfe eines interaktiven Theorembeweisers nachzuweisen (zu "verifizieren"), um so die Zuverlässigkeit des Model Checking selbst signifikant zu erhöhen. Neben den monolithischen Model Checkern selbst werden wir auch eine Reihe von einzeln verwendbaren, verifizierten, grundlegenden Komponenten bereitstellen wie etwa einen Äquivalenzchecker oder Determinisierungsverfahren für Automaten auf unendlichen Wörtern.Der erste Model Checker soll vor allem auf hohe Performanz hin entwickelt werden und mit dem weit verbreiteten (aber nicht verifizierten) Model Checker SPIN konkurrenzfähig sein, was hohe Anforderungen an die Effizienz der Algorithmen stellt und die Korrektheitsbeweise anspruchsvoller macht. Der Schwerpunkt liegt hier auf dem Übergang zu imperativen und platzeffizienten Datenstrukturen.Der zweite Model Checker soll auf eine erweiterte Klasse von Systemen anwendbar sein, die probabilistisches Verhalten zeigen können und deren Eigenschaften daher nur mit bestimmten Wahrscheinlichkeiten garantiert werden können. Beim probabilistischen Model Checker liegt der Schwerpunkt auf der Kombination verifizierter graphentheoretischer, automatentheoretischer und numerischer Algorithmen. Hier sollen erstmal Löser für lineare Gleichungssysteme und lineare Programme verifiziert werden. Allerdings wollen wir so weit wie möglich auf existierende und über eine lange Zeit hin optimierte Löser aufbauen. Daher werden wir verifizierte Werkzeuge entwickeln um die Ausgaben solcher Löser, die meist approximativ sind, auf Korrektheit innerhalb einer gewissen Fehlertoleranz zu überprüfen. Dies ist nur Dank spezifischer Eigenschaften unserer Gleichungssysteme bzw linearen Programme möglich.

• DFG-Verfahren: Sachbeihilfen
• Mitverantwortliche: Professor Dr. Javier Esparza; Dr. Michael Luttenberger; Professor Tobias Nipkow, Ph.D.