Abschlussarbeiten

Im Folgenden sind Themengebiete in denen wir Projekt- und Abschlussarbeiten anbieten kurz zusammengefasst. Es gibt (fast) immer aktuelle, konkrete Themen für Abschlussarbeiten in den genannten Bereichen. Des Weiteren finden Sie am Ende dieser Seite eine Auswahl konkreter Projekt- und Abschlussarbeitsthemen. Wenn Sie Interesse an einem der Themen bzw. Themengebiete oder weitere Ideen haben, vereinbaren Sie doch einen Termin mit einem unserer Mitarbeiter per E-Mail. Ebenso, wenn Sie an einer Stelle als studentische/r Mitarbeiter/in ("HiWi") in diesen Bereichen interessiert sind.

Themengebiete

Sollte Sie keines der im Folgenden ausgeschriebenen Themen ansprechen, sprechen Sie einen unserer Mitarbeiter auf weitere Themen an. Ebenso wenn Sie eigene Themenideen haben.

Fallstudien

Zur Evaluation und zum Vorantreiben unserer Ansätze wollen wir möglichst viele Fallstudien durchführen. Zu den interessanten Fallstudien im Moment zählen:

  • Das Java Collection Framework
  • Funktionale Eigenschaften von E-Voting-Systemen
  • Verifikation von (abstrakten) Algorithmen, z. B. Graph-Traversierung
  • Die Verifikation von veröffentlichten "Verification Challenges"

Ansprechpartner: Mattias Ulbrich

Involvierte Forschungsprojekte: KeY-Projekt, DeduSec

Verifikationsansätze

In der Verifikation ist die Frage, welche Speicherbereiche von einem Program modifiziert werden dürfen, von zentraler Bedeutung. Wir suchen eine/n Master-Studierende/n, der/die sich in einer Projekt- oder Abschlussarbeit mit verschiedenen Ansätzen beschäftigt und ihre Möglichkeiten (Ausdrucksstärke, Einsetzbarkeit, etc.) vergleicht.

Ansprechpartner: Mattias Ulbrich

Involvierte Forschungsprojekte: KeY-Projekt

Fairness in Social-Choice-Mechanismen

Social-Choice-Mechanismen sind Algorithmen zur Lösung von Problemen kollektiver Entscheidungsfindung wie bei politischen Wahlen oder der fairen Ressourcenverteilung (bspw. beim Datenverkehr im Internet). Gesetzestexte geben hier bspw. Vorgaben wie "Jede Stimme ist gleich." oder "Meine Daten sollen nicht benachteiligt werden.".
Aber wie lässt sich nachweisen, dass die entsprechenden Wahl- oder Routingverfahren dies wirklich erfüllen? Sind die gestellten Anforderungen eventuell von keinem Verfahren erfüllbar? Wir suchen motivierte Bachelor- und Master-Studierende zur Formalisierung entsprechender Anforderungen und Entwicklung von Ansätzen, deren Unerfüllbarkeit bzw. Korrektheit bzgl. Algorithmen formal zu verifizieren, sowie zur Analyse konkreter Fallstudien.

Ansprechpartner: Michael Kirsten

Involvierte Forschungsprojekte: COMSOC, KeY-Projekt

Testen von Sicherheitseigenschaften für IT-Systeme

Die Verifikation von Sicherheitseigenschaften kann sehr aufwändig sein, daher möchten wir untersuchen, wie man die Sicherheit von Software durch einfachere Techniken wie die automatische Generierung von Testfällen zeigen kann.
Doch wie sehen solche Testfälle aus und wie lassen sich Kriterien der Testabdeckung auf Sicherheitseigenschaften übertragen? Alternativ ist denkbar, automatisch Exploits zu generieren, die einen möglichen Angreifer simulieren und im Erfolgsfall eine Sicherheitslücke aufdecken können. Zur Bearbeitung dieser Fragestellungen suchen wir motivierte Bachelor- und Master-Studierende.

Ansprechpartner: Mihai Herda

Involvierte Forschungsprojekte: DeduSec, KASTEL

Usability von Werkzeugen zur deduktiven Software-Verifikation

Ansprechpartner: Sarah Grebing

Involvierte Forschungsprojekte: KeY-Projekt

Verifikation für Industrieanlagen

Im Zeitalter von Industrie 4.0 werden Industrieanlagen zunehmend komplexer. Dennoch müssen sie Sicherheitsaspekte (Safety und Security) gewährleisten. Hier setzen wir formale Verifikation ein, um diese Eigenschaften zu garantieren. Wir erforschen Regression Verification um Eigenschaften über die Evolution von Software hinweg sicherzustellen, außerdem untersuchen wir Sicherheitsangriffe auf Produktionsanlagen.
Für beide Aspekte suchen wir motivierte Bachelor- oder Master-Studierende, die entsprechende Themenstellungen bearbeiten.

Ansprechpartner: Alexander Weigl

Involvierte Forschungsprojekte: IMPROVE APS, KASTEL

Themenvorschläge

Neben den obigen Themengebieten sind die unten aufgeführten Arbeiten und Projekte zu vergeben.

Beendete und laufende Projekt- und Abschlussarbeiten
Titel Typ Betreuer Bearbeiter
Probablistische Beweis-Analyse mit KeY MA Mattias Ulbrich
Mihai Herda
Stefan Kobischke
Effiziente Produkt-Programme für Java BA Michael Kirsten
Mattias Ulbrich
Pascal Gabriel
Integrating Bounded Model Checking with KeY MA Mattias Ulbrich
Michael Kirsten
(vorgemerkt bis März 2018)
Exploration of Failed Proof Attempts BA Sarah Grebing Thomas Trapp
JML-Java Parser BA Alexander Weigl
Flexible Term and Formula Matching BA Sarah Grebing abgeschlossen
A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification BA Michael Kirsten
Mattias Ulbrich
Florian Lanzinger
Applying Bounded Verification to the German Seat Distribution Procedure BA Michael Kirsten Grigori Schapoval
Applying Relational Techniques for the Deductive Verification of Voting Systems BA Thorsten Bormer
Mattias Ulbrich
Michael Kirsten
Till Neuber
Formalisierung von Verhaltensdifferenzen in Automatisierungssoftware BA Mattias Ulbrich
Alexander Weigl
Kevin Zhang
Zustandsfolgenbasierte Programmverifikation SA Daniel Grahl Andreas Wagner
Verifiziert sicherer Informationsfluss mit Events BA Daniel Grahl
Verifikation von Dafny-Programmen DA Daniel Grahl
Verification-based Test Generation BA / SA / MA / DA Christoph Gladisch
Model Generation SA / BA / MA / DA Christoph Gladisch
Hybrid Systems Verification:
Autonome Navigation von mobilen Robotern
BA Bernhard Beckert David Vogelbacher
Effiziente Verifikation von Informationssicherheit BA Daniel Grahl Fabian Ruch
Combining Graph-Based and Deductive Information-Flow Analysis for Proving Non-Interference PdF Mihai Herda
Michael Kirsten
Marko Kleine Büning
Formale Verifikation objektorientierter Software für Produktionsanlagen PdF Alexander Weigl
Mattias Ulbrich
Augusto Modanese
MA = Masterarbeit, BA = Bachelorarbeit, DA = Diplomarbeit, SA = Studienarbeit, PdF = Praxis der Forschung