Leitung

Prof. Dr. Heike Wehrheim

Kontakt

Sekretariat

Marion Bramkamp

Uhlhornsweg 84 — Raum A2 2-228

+49 441 798-4522

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.

Identity Transformations for Software Verification Testing

Motivation

Incorrectness logics [1] (or reachability logics) can be seen as the dual to correctness logics like those underlying Hoare-like proof calculi. Incorrectness proof calculi reason about the reachability of errors in some executions whereas correctness calculi reason about the safety of all executions.

The task of this Master thesis is the extension of an existing incorrectness logic [1] for sequential programs to parallel programs. This extension should follow the idea of considering interleavings of parallel components, along the lines of [2] which has developed an incorrectness separation logic. There is no need, however, to understand separation logics.

Helpful (but not required) prerequisite: Course Program Verification of Prof. Olderog.

 

[1] Peter W. O'Hearn: Incorrectness logic. Proc. ACM Program. Lang. 4(POPL): 10:1-10:32 (2020).

[2] Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn: Concurrent incorrectness separation logic. Proc. ACM Program. Lang. 6(POPL): 1-29 (2022).

Contact: Heike Wehrheim

Lokalität von Persistenter Linearizierbarkeit

Beschreibung

 
Linearizierbarkeit ist ein Korrektheitkriterium für nebenläufige Datenstrukturen wie Keller oder Schlangen. Linearizierbarkeit garantiert, dass sich eine parallel genutzte Datenstruktur immer so verhält, als würde sie ihre Operationen atomar, sequentiell, eine nach der anderen ausführen. Eine wichtige Eigenschaft von Linearizierbarkeit ist Lokalität: wenn Datenstrukturen alleine linearizierbar sind, dann auch immer die gemeinsame Nutzung mehrerer Datenstrukturen.
Seit kurzem gibt es eine Erweiterung von Linearizierbarkeit, die bei persistentem Speicher Anwendung findet. Persistenter oder auch non-volatiler Speicher ist eine neue Speichertechnologie, bei der Daten im Hauptspeicher auch bei einem Systemcrash nicht verloren gehen. Für Persistente Linearizierbarkeit (oder auch englisch durable linearizability) und eine Abschwächung davon (buffered durable linearizability) ist bekannt, dass sie lokal bzw. nicht lokal ist; ein formaler Beweis fehlt aber bisher.
Die Aufgabe der Arbeit liegt nun darin, (a) solche existierenden Korrektheitskriterien formal in einem einheitlichen Rahmen zu definieren, sowie (b) für jede der Kriterien einen Beweis der Lokalität oder ein Gegenbeispiel anzugeben.

Literatur:
[1] Herlihy, Wing: Linearizability: A correctness condition for concurrent objects, ACM TOPLAS, Vol.12, No.3, 1990.
[2] Israelevitz, Mendes, Scott: Linearizability of persistent memory objects under a full-system-crash failure model, in: DISC 2016.

Kontakt: Heike Wehrheim

 

Simulation einer operationellen Semantik eines schwachen Speichermodells

Beschreibung

Schwache Speichermodelle beschreiben die Ausführung von parallelen Programmen auf modernen Multicore Architekturen. Die Semantik der Programme kann beispielsweise durch operationelle Semantiken angegeben werden. Diese sind oft recht komplex und müssen manuell für gegebene Programme abgearbeitet werden.
Die Aufgabe der Bachelorarbeit ist nun die Entwicklung und Implementierung eines Simulators für eine solche Semantik. Der Simulator soll es erlauben, die Programmausführung in eine bestimmte Richtung zu steuern. Idealerweise würde der Simulator es außerdem erlauben, die Semantik leicht ändern zu können, und dann Simulation für die geänderte Semantik anbieten.

Um ein Gefühl für die Art der Semantik zu bekommen, kann ein Blick in [1] geworfen werden. Daran sieht man gut die Komplexität der Semantiken, von der man sich aber nicht abschrecken lassen sollte (es wird Hilfe beim Verstehen geben).

Literatur:
[1] Christopher Pulte et al.: Promising ARM/RISC-V: A simpler and faster operational concurrency model, PLDI 2019.

Kontakt: Heike Wehrheim

 

Kooperative Software-Verifikation durch Austausch von Bereichen

Motivation

Eine Kernidee der Kooperative Software-Verifikation ist, den Workload einer gemeinsamen  Verifikationsaufgabe auf mehrere Verifizierer zu verteilen. Eine Möglichkeit ist die Fragmentierung des Programms in mehrere Teile, wobei jedes Fragment unabhängig voneinander analysiert wird. Ranged Symbolic Execution [1] hat gezeigt, dass dies für die Symbolic Execution effektiv möglich ist. Dieser Erfolg soll nun von Ranged Symbolic Execution auf allgemeine Verifikationstechniken übertragen werden.

Inhalt & Ziele

Bei der Ranged Symbolic Execution wird ein Programm in mehrere Teile aufgeteilt, indem ein Analysebereich definiert wird. Hier wird ein Bereich durch zwei Testeingaben definiert, die Ausführungspfade innerhalb des Programms widerspiegeln. Die Symbolic Execution analysiert dann nur den Teil des Programms, der innerhalb des vorgegebenen Bereichs liegt.

Das Ziel dieser Arbeit ist es nun, diese Idee für beliebige Verifikationstechniken zu verallgemeinern (Ranged Execution). Als Teil dieser Arbeit soll Ranged Execution als konfigurierbare Programmanalyse (CPA) formalisiert und in das Verifikationsframework CPAchecker implementiert werden. Es ist auch wünschenswert, die Idee der Ranged Execution theoretisch mit bestehenden Methoden der kooperativen Verifikation (z.B. Conditional Model Checking [2]) zu verbinden.

Während die Bachelorarbeit theoretisch motiviert ist, ist eine Arbeit mit praktischerem Fokus denkbar (z.B. durch empirische Evaluierung verschiedener Kombinationen von Verifizierern).

 

[1] Junaid Haroon Siddiqui and Sarfraz Khurshid. 2012. Scaling symbolic execution using ranged analysis. In Proc. OOPSLA
[2] Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, and Philipp Wendler. 2012. Conditional model checking: a technique to pass information between verifiers. In Proc. ICSE

 

Kontakt: ,

 

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: ,

 

Aktives Lernen für Invarianten

Motivation

Das Finden von korrekten und hilfreichen Invarianten ist eine der Kernaufgaben bei der Softwareverifikation. In den letzten Jahren wurden verschiedene Ansätze zur Invarianten-Generierung vorgestellt, die verschiedene Machine Learning Techniken verwenden, darunter von Li et al. [1], die in Ihrer Arbeit einen aktiven Lernalgorithmus auf Basis einer Support-Vektor Maschine verwenden.  Um die verschiedenen Ansätze vergleichen zu können, wurde das MIGML Framework entwickelt. In diesem Framework lassen sich verschiedenen Techniken abbilden und damit vergleichen. Allerdings ist das MIGML Framework aktuell nur in der Lage, passive Lernalgorithmen zu unterstützen. Daher kann der Ansatz von Li et al. Nicht abgebildet werden.

 

Inhalt und Ziele

In dieser Arbeit soll das existierende MIGML Framework konzeptionell erweitert werden, um aktive Lernalgorithmen zu unterstützen, sodass der oben genannte Ansatz im Anschluss durch das MIGML Framework abgebildet werden können. Neben der Implementierung der konzeptionellen Erweiterung muss der in der Arbeit verwendete Lernalgorithmus implementiert werden, wobei für die Realisierung existierende Komponenten von MIGML wiederverwendet werden können.
Im Anschluss soll in einer umfangreichen Evaluation die Performance des neuen Ansatzes  (1) mit den existierenden Ansätzen in MIGML und (2) anderen Tools zur Invariantengenrierung / Verifikation verglichen werden.

[1] Jiaying Li, Jun Sun, Li Li, Quang Loc Le, and Shang-Wei Lin. 2017. Automatic loop-invariant generation and refinement through selective sampling. In Proc. ASE 2017.

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:

Testen von WEKA ML-Algorithmen für Ausgewogene Datennutzung

Motivation

In dieser Zeit wurden in mehreren Anwendungsdomänen verstärkt Modelle des maschinellen Lernens (ML) verwendet.  Mit der Verfügbarkeit von Daten und der Weiterentwicklung von ML-Algorithmen ist es nun möglich,  solche Modelle in Softwaresystemen zur kritischen Entscheidungsfindung zu verwenden. Da diese Modelle in solchen Systemen häufig verwendet werden, kommt natürlich die Qualitätssicherung solcher Modelle in Frage.  Dies hat viele Forscher dazu veranlasst, sich mit dem Thema der Validierung und Verifizierung von  ML-Modellen in Bezug auf Eigenschaften wie Fairness, Monotonie, Robustheit usw wird zuvor verwendet, um aus Trainingsdaten zu „lernen“ und solche ML-Modelle zu generieren.

Inhalt und Ziele

In einer früheren Arbeit [1] entwickeln wir ein metamorphes Testwerkzeug TiLe (in Python) für ML-Algorithmen. Die Hauptidee dieses Testrahmens besteht darin, mehrere metamorphe Transformationen auf die Trainingsdaten anzuwenden und herauszufinden, ob das gelernte Modell vor und nach der Anwendung solcher Transformationen gleich ist. Ein Beispiel für eine solche Transformation ist die zufällige Permutation der Trainingsdateninstanzen.

Das Hauptziel dieser Arbeit wäre es, TiLe zu verwenden, um die ML-Algorithmen aus der WEKA zu validieren, um herauszufinden, ob sie für solche Transformationen der Trainingsdaten empfindlich sind. Zunächst soll das Tool für die Arbeit mit den ML-Algorithmen in Java erweitert werden. Dann würden mehrere andere mögliche metamorphe Transformationen (zum Beispiel für die Vorverarbeitung von Trainingsdaten) in Betracht gezogen. Schließlich würde im Gegensatz zu den vorherigen Arbeiten, bei denen wir häufig Zufallstests verwenden, um die Äquivalenz von Modellen herauszufinden, eine verbesserte (bereits entwickelte) Validierungstechnik in das Tool integriert werden.
Bitte beachten Sie, dass dieses Thema nur für Bachelorarbeiten berücksichtigt werden kann.

1.  Arnab Sharma and Heike Wehrheim. Testing machine learning algorithms for balanced data usage. In 12th IEEE Conference on Software Testing, Validation and Verification, ICST, pages 125–135, 2019.

Kontakt: Arnab Sharma

(Stand: 07.06.2022)