Leitung

Prof. Dr. Heike Wehrheim

Kontakt

Sekretariat

Marion Bramkamp

Uhlhornsweg 84 — Raum A3 2-208

+49 441 798-2426

Abschlussarbeiten

Wir bieten verschiedene Themen für Bachelor und Masterarbeiten an. Die folgende Liste enthält einige Vorschläge. Bei Interesse an einer Arbeit in unserer Gruppe können Sie auch gerne direkt jemanden aus der Gruppe ansprechen.

Identitätstransformationen zum Testen von Verifikationswerkzeugen

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.

Kontakt: ,

 

Klassifikation von Online-Verifikationsmerkmalen

Motivation:
Ziel der Softwareverifikation ist es, zu beweisen oder zu widerlegen, ob ein Programm eine Spezifikation erfüllt. Viele Ansätze erforschen dabei den Zustandsraum des Programms oder berechnen Prädikate zur Abstraktion des Zustandsraums.
Im Fall eines fehlerhaften Programmes, neigen jedoch viele bestehende Techniken dazu, ihre Zeit mit der Erkundung korrekter Teile des Programmes zu verschwenden.  Eine Anpassung des Suchstrategie oder das Wechseln zu einem anderen Verifikationsalgorithmus könnte in diesen Fällen von Vorteil sein. 
Mit der Hilfe von maschinellem Lernen soll ein Algorithmus entwerfen, der diese Situationen während der Verifikation erkennt.

Ziele & Inhalt der Arbeit:
Die Erfassung relevanter Daten und die Erstellung eines aussagekräftigen Datensatzes ist ein wesentlicher Bestandteil datengetriebener Algorithmen. Ziel dieser Arbeit ist daher die automatische Generierung eines Datensatzes zum Lernen von Verifikationsverhalten.
Zu diesem Zweck sollte eine Technik entwickelt und implementiert werden, die das Suchverhalte bzw. die generierten Prädikate eines Verifikationsalgorithmus analysiert, relevante Ereignisse identifiziert und die gesammelten Informationen in einem geeigneten Format speichert.
Der entwickelte Ansatz soll dann in das Verifikationsframework CPAchecker integriert werden, welches uns auch die notwendigen Verifikationsalgorithmen liefert. Letztendlich soll die neuartige Technik zur Erzeugung eines Datensatzes eingesetzt werden, während die Performanz und Qualität des Generierungsprozesses evaluiert werden soll. Außerdem sollen einfache Entscheidungsregeln zur Vorhersage der Erfolgswahrscheinlichkeit definiert werden.

Es ist auch möglich, das Thema im Rahmen einer Masterarbeit zu bearbeiten. In diesem Fall ist die Datengenerierung nur der erste Teil. In einem zweiten Teil soll ein maschineller Lernalgorithmus entwickelt werden, der die Erfolgswahrscheinlichkeit der aktuellen Verifikation voraussagt. Der Lernalgorithmus soll dann in Bezug auf Accuracy und Laufzeit evaluiert werden.

Kontakt:

(Stand: 09.06.2021)