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

Gesellschaftliche Anforderungen an Social-Choice-Mechanismen

Social-Choice-Mechanismen sind Algorithmen zur Lösung von Problemen wie Präferenzaggregation oder Ressourcenallokation, bspw. im Kontext von demokratischen Wahlen, oder für Netzwerke wie dem Internet. Offizielle Dokumente wie z. B. Gesetzestexte geben hier Anforderungen wie "Jede Stimme ist gleich." oder "Meine Daten sollen nicht benachteiligt werden." vor.
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 Master-Studierende (in Ausnahmefällen auch Bachelor-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
Formalisierung von Verhaltensdifferenzen in Automatisierungssoftware DA / BA / MA Mattias Ulbrich
Alexander Weigl
Kevin Zhang
Zustandsfolgenbasierte Programmverifikation SA Daniel Grahl
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
Formale Verifikation objektorientierter Software für Produktionsanlagen PdF Alexander Weigl
Mattias Ulbrich
Augusto Modanese
Hybrid Systems Verification:
Autonome Navigation von mobilen Robotern
MA / DA Bernhard Beckert David Vogelbacher
Model Generation SA / BA / MA / DA Christoph Gladisch
Effiziente Verifikation von Informationssicherheit BA Daniel Grahl
MA = Masterarbeit, BA = Bachelorarbeit, DA = Diplomarbeit, SA = Studienarbeit, PdF = Praxis der Forschung