Motivation

Software-Verifikationswerkzeuge wie CPAchecker werden immer effektiver bei der Überprüfung der Korrektheit von C-Programmen oder beim Auffinden von Programmfehlern. Ein wichtiger Faktor für den Fortschritt von Verifikationswerkzeugen ist das Vorhandensein von groß angelegten Benchmarks, die sowohl die Fortschritte dieser Werkzeuge als auch ihre Schwächen aufzeigen. Die vorhandenen Benchmarks sind jedoch in ihrer Größe begrenzt und können nur einen begrenzten Teil der Fähigkeiten der Verifizierungswerkzeuge testen. 

Aus diesem Grund ist es das Ziel dieser Masterarbeit, einen automatischen Ansatz für die Konstruktion neuer Verifikationsbenchmarks zu entwickeln. Die Idee ist, dass wir bestehende Verifikationsbenchmarks in Benchmark-Bausteine zerlegen können und diese Bausteine dann kombiniert werden können, um neue Benchmarks zu erstellen.

Die größte Herausforderung besteht darin, einen Zerlegungs- und Zusammensetzungsprozess zu konstruieren, der die Korrektheit des resultierenden Benchmarks garantiert (d.h. wenn die ursprünglichen Benchmarks einen Fehlerpfad enthalten, sollte der Ansatz garantieren, dass der konstruierte Benchmark ebenfalls einen Fehlerpfad enthält).