Bei Softwareverifikation geht es darum, zu zeigen, dass ein Programm, auf eine bestimmte Eigenschaft bezogen, korrekt ist oder einen Fehler enthält. Für diese Verifikationsaufgaben gibt es unterschiedliche Verifikationstools, wie zum Beispiel der CPAchecker, deren Leistung anhand von Benchmarks ermittelt wird.
Diese Tools nutzen häufig Heuristiken, um in Verifikationsaufgaben möglichst schnell und korrekt Ergebnisse erzielen zu können. Dies kann jedoch dafür sorgen, dass unerwartet inkorrekte Ergebnisse zurückgegeben werden. In der BA sollen eine Reihe von Tools auf ihre Konsistenz getestet werden, indem korrekte Programme so modifiziert werden, dass sie nach dieser Transformation weiterhin korrekt sind. Diese Transformationen basieren auf dem Entfernen von Pfaden aus dem Abstract Reachability Graphs (ARG). Durch die Verwendung von Heuristiken ist jedoch nicht garantiert, dass die Programme weiterhin als korrekt identifiziert werden können. Die Aufgaben der Abschlussarbeit bestehen darin, entsprechende Transformationen umzusetzen, ein kleines Benchmarkset zu generieren und ausgewählte Verifikationstools darauf zu testen.