Motivation

Verifikationswerkzeuge, wie zum Beispiel CPAchecker, werden immer effektive in der Verifizierung von C-Programmen oder in dem Finden von Programmierfehlern. Trotzdem existieren erstaunlich kleine Programme, auf dennen die meisten Verifizier scheitern. Die Ursache ist häufig unklar und kann möglicherweise auf ein komplexes Zusammenspiel von Programelemten (z.B. verschachtelte Schleifen zusammen mit Zeigern und Arrays) zurückgeführt werden. Ohne eine klare Intuition wird die Weiterentwicklung bestehender Verifier jedoch immer schwieriger.

Inhalt & Ziele

Mit dieser Arbeit möchten wir die ersten Schritte unternehmen, um das Verhalten eines Verifizieres zu verstehen und Fehlerquellen zu identifizieren. Basierend auf einfachen C-Programmen mit einem klarem und vom Menschen überprüfbaren Verifikationsziel, soll eine Reihe von Identitätstransformation entwickelt werden. Eine Identitätstransformation verändert den Code, sodass die Programmsemantik sich nicht ändert, aber die Verifikationsschwierigkeit erhöht wird. Ein Beispiel für eine solche Transformation könnte wie folgt aussehen: int a = 5; -> int a; int b = 5; a = b;

Wir bieten diese Arbeit als Bachelor- oder Masterarbeit an. Im Rahmen einer Bachelorarbeit sollen folgende Ziele erreicht werden:

• ein generelles Framework für einfache Identitätstransformationen auf C-Code (z.B. via String matching)
• die Implementierung einiger einfacher Identitätstransformationen, die zentrale Programmfeatures der C-Sprache addressieren
• die Generierung eines Benchmarks und die Evaluierung von CPAchecker auf dem Benchmark

Sollte die Arbeit für ein Masterabschluss geschrieben werden, soll noch zusätzlich folgende Ziele erreichen werden:

• die Entwicklung und Implementierung von komplexen Identitätstransformationen (z.B. via AST Transformationen)
• die Entwicklung einer größeren Menge von Basisprogrammen
• die Durchführung einer größer angelegten Studie auf generierten Benchmarks und der Evaluierung von mindestens 3 State-of-Art Verifikationswerkzeugen.