Fehler, die in Programmen oder in der Hardware eines Gerätes auftreten, können viele negative Folgen für unseren Alltag haben. Die Konsequenzen variieren dabei von ärgerlichen Kleinigkeiten bis hin zu gefährlichen oder sogar katastrophalen, lebensbedrohlichen Situationen. Um solche Fehler möglichst zu vermeiden, gibt es Verifikationsprogramme, die versuchen, Fehler in Software und in Hardware zu finden. Die Verifikationsprogramme erhalten als Eingabe eine Beschreibung des zu überprüfenden Objekts. Allerdings sind diese Beschreibungen oft sehr groß, und daher haben die Verifikationsprogramme oft einen enormen Speicherplatzbedarf und es dauert sehr lange, bis sie eine Antwort geben, was den Entwicklungsprozess verlangsamt und verteuert. Bisweilen sind die Eingaben sogar so groß, dass keine Analyse oder zumindest keine vollständige Analyse möglich ist.
In diesem Forschungsprojekt haben wir daher neue Algorithmen für Verifikationsprogramme entwickelt, die weniger Laufzeit und auch weniger Speicherplatz benötigen, damit größere Objekte überprüft werden können. Diese Algorithmen können nicht nur einfache Fehler, sondern auch komplexe Fehler schneller als bisher finden. Dabei haben wir nicht nur unsere neuen Algorithmen theoretisch analysiert, sondern auch implementiert. Unsere Verifikationsalgorithmen verwenden zum Teil neu entwickelte Techniken und zum Teil auch Techniken, die schon in anderen Bereichen der Algorithmenforschung zum Einsatz kamen.
Des weiteren haben wir gezeigt, dass unsere Algorithmen nicht nur Anwendungen in Computerverifikation haben, sondern auch in probabilistischen Planungsproblemen und künstlicher Intelligenz.