Abschlussarbeiten

Im Folgenden sind Themengebiete in denen wir Projekt- und Abschlussarbeiten anbieten kurz zusammengefasst. 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.

Offene Projekt- und Abschlussarbeiten
Titel Typ Betreuer Bearbeiter
Effiziente Produkt-Programme für Java BA Mattias Ulbrich
Michael Kirsten
JML-Java Parser BA Alexander Weigl
Integrating Bounded Model Checking with KeY MA Mattias Ulbrich
Michael Kirsten
Flexible Term and Formula Matching BA Sarah Grebing
Effizienter Umgang mit Zeitkonstanten in der Verifikation reaktiver Systeme MA Mattias Ulbrich
Alexander Weigl
Exploration of Failed Proof Attempts BA Sarah Grebing
Schwergewichtige Blockkontrakte für KeY BA / MA Mattias Ulbrich
Michael Kirsten
Entwicklung eines formalen Fairnessmodells für Datenverkehr MA Michael Kirsten
Formalisierung und Verifikation des deutschen Wahlrechts BA / MA Michael Kirsten
Nichtinterferenz in relationalen Datenbanksystemen PdF Simon Greiner
Scripting Interactive Proofs MA / DA Sarah Grebing
Mattias Ulbrich
Beendete und laufende Projekt- und Abschlussarbeiten
Titel Typ Betreuer Bearbeiter
Formalisierung von Verhaltensdifferenzen in Automatisierungssoftware DA / BA / MA 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
Effiziente Verifikation von Informationssicherheit BA Daniel Grahl Fabian Ruch
Hybrid Systems Verification:
Autonome Navigation von mobilen Robotern
MA / DA Bernhard Beckert David Vogelbacher
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