Parallele Software Verifikation

Dieses Forschungsthema untersucht, in wie weit sich zentrale Algorithmen der Software Verifikation auf modernen Hardwarearchitekturen, wie sie in aktuellen Mehrkern- und Grafikprozessoren zu finden sind, effizient parallelisieren lassen. Unser Fokus liegt derzeit auf parallelen Lösern für große Boolsche Gleichungssysteme, die aus Millionen von Gleichungen und Variablen bestehen. Solche Gleichungssysteme sind der Grundpfeiler für eine Fülle von Verfahren der Software Verifikations und Analyse, wie z. B. Model Checking, Datenflussanalyse, Equivalenzprüfung und Testfallerzeugung. In Anbetracht dieser vielfältigen Anwendungsgebiete ist zu erkennen, dass das effiziente Lösen von Boolschen Gleichungssystemen von hoher praktischer Relevanz ist.

Unser Ansatz erforscht die Eignung verschiedener paralleler Algorithmen und Datenstrukturen zum Speichern und Lösen Boolscher Gleichungssysteme. Durch Ausnutzung der einfachen und einheitlichen Struktur dieser Systeme soll deren Lösung beschleunigt werden. Dabei werden vielfältige Ansätze untersucht, von der Gauß Elemination bis hin zu Graph basierten Verfahren. Eine anvisierte Anwendung ist die Überprüfung großer Softwaremodelle in Hinblick auf Eigenschaften des Programmverhaltens, mit dem Ziel Softwareentwicklern wichtige Hinweise zu Programmfehlern möglichst schnell zu liefern. 

Kontakt: Prof. Dr. Gerald Lüttgen