Moderne Graphalgorithmen für die formale Verifikation

Abstract

In der formalen Verifikation versucht man Fehler von Systemen automatisch zu finden. Ein Modellprüfer kontrolliert ob ein gegebenes Modell eines Systems eine Anforderung erfüllt. In der reaktiven Synthese wird mit einer gegebenen Anforderung ein korrektes reaktives System erzeugt. Wir verbinden das Gebiet der modernen theoretischen Graphalgorithmen mit dem Gebiet der formalen Verifikation indem wir schnellere Algorithmen für algorithmische Probleme in der Modellprüfung und der reaktiven Synthese in der Dissertation vorstellen. Neben gewohnten “expliziten” Algorithmen stellen wir symbolische Algorithmen vor – Symbolische Algorithmen erlauben zwar nur einen limitierten Zugang zur Eingabe, ermöglichen aber eine effizientere Speicherrepräsentation.