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. Desweiteren finden Sie am Ende dieser Seite eine Auswahl konkreter Projekt- und Abschlussarbeitsthemen. Wenn Sie Interesse an einem der Themen bzw. Themengebiete haben oder wenn Sie an einer Stelle als studentische/r Mitarbeitende/r ("HiWi") in diesen Bereichen interessiert sind, vereinbaren Sie doch einen Termin mit einem/r unserer Mitarbeitenden per E-Mail.
Themengebiete
Sollte Sie keines der im Folgenden ausgeschriebenen Themengebiete ansprechen, sprechen Sie eine/n unserer Mitarbeitenden auf weitere Themen an. Das gleiche gilt, 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"
Ansprechperson: 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.
Ansprechperson: Mattias Ulbrich
Involvierte Forschungsprojekte: KeY-Projekt
Fairness von Social-Choice-Mechanismen
Social-Choice-Mechanismen sind Algorithmen zur Lösung von Problemen kollektiver Entscheidungsfindung
wie etwa politische Wahlen oder faire Ressourcenverteilung (bspw. beim Datenverkehr im Internet).
Gesetzestexte geben hier Vorgaben wie "Jede Stimme ist gleich." oder "Meine Daten sollen nicht
benachteiligt werden.".
Aber wie lässt sich nachweisen, dass die Wahl- oder Routingverfahren dies
wirklich erfüllen? Sind die gestellten Anforderungen eventuell von keinem Verfahren erfüllbar?
Wir suchen motivierte Bachelor- und Masterstudieren-de zur Formalisierung entsprechender
Anforderungen und Entwicklung von Ansätzen, deren Unerfüllbarkeit bzw. Korrektheit
bzgl. Algorithmen formal zu verifizieren, sowie zur Analyse konkreter Fallstudien.
Zur Motivation der Thematik im Kontext von Wahlverfahren empfehlen wir ein veranschaulichendes
Video der Universität von Amsterdam.
Ansprechperson: Michael Kirsten
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.
Ansprechperson: Alexander Weigl
Involvierte Forschungsprojekte: IMPROVE APS, KASTEL
Verifikation von Smart Contracts
Im Zusammenhang mit Distributed-Ledger-Technologie spielen Smart Contracts zunehmend eine Rolle: Programme, die auf einer Blockchain laufen und dort beispielsweise die Kontrolle über Güter übernehmen. Weil Smart Contracts nach der Veröffentlichung nicht oder nur schwer verändert werden können und zudem meist öffentlich einsehbar sind, sind die Anforderungen bezüglich funktionaler Korrektheit hier besonders hoch, und der Einsatz formaler Methoden zum Beweis wichtiger Eigenschaften ist oft unerlässlich. In diesem Zusammenhang stellt sich einerseits die Frage, wie konkrete Implementierungen von Smart Contracts (beipielsweise in Hyperledger Fabric oder Ethereum) spezifiziert und verifiziert werden können. Andererseits soll erforscht werden, wie sich Smart Contracts formal modellieren lassen.
Ansprechperson: Jonas Schiffl
Involvierte Forschungsprojekte: KASTEL
Themenvorschläge
Neben den obigen Themengebieten sind die unten aufgeführten Arbeiten und Projekte zu vergeben.
Sollte Ihnen keines der im Folgenden aufgelisteten Themen zusagen, dann kommen Sie gerne mit Ihren Ideen
(vorzugsweise – aber nicht ausschließlich – im Rahmen der Themengebiete oben oder
Forschungsinteressen der jeweiligen Mitarbeiterinnen oder Mitarbeiter) auf uns zu.