Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

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 Themengebiete 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 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 Routing-Verfahren dies wirklich erfüllen? Sind die gestellten Anforderungen eventuell von keinem Verfahren erfüllbar? Wir suchen motivierte Bachelor- und Master-Studierende zur Formalisierung entsprechen- der Anforderungen und Entwicklung von Ansätzen, deren Unerfüll-barkeit bzw. Korrektheit bzgl. Algorithmen formal zu verifizieren, sowie zur Analyse konkreter Fallstudien.

Ansprechpartner: Michael Kirsten

Involvierte Forschungsprojekte: COMSOC, KeY-Projekt

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.
Sollte Ihnen keines der im Folgenden aufgelisteten Themen zusagen, dann kommen Sie gerne mit Ihren Ideen (vorzugsweise – aber nicht aus-schließlich – im Rahmen der Themengebiete oben oder Forschungsinteressen der jeweiligen Mitarbeiterinnen oder Mitarbeiter) auf uns zu.

Offene Projekt- und Abschlussarbeiten
Titel Typ Betreuer Bearbeiter
Verify Your Favourite Voting Rule BA / MA Michael Kirsten
Program Synthesis from Generalised Test Tables MA / PdF Alexander Weigl
Verification of a Distributed Floodfill Implementation MA Mattias Ulbrich
Using SDGs to Generate Frame Conditions BA Mihai Herda
Verification of Efficient Arithmetic Operations BA Mattias Ulbrich
Semantics of Sequential Function Charts BA Alexander Weigl
Property-Directed Reachability for Regression Verification MA / PdF Alexander Weigl
Test Coverage of Generalised Test Tables BA Alexander Weigl
Bislicing – Slicing for Relational Verification MA / PdF Mattias Ulbrich
Mihai Herda
Automated Correct Algorithm Transformation into Map Reduce MA Mattias Ulbrich
Effizienter Umgang mit Zeitkonstanten in der Verifikation reaktiver Systeme MA Mattias Ulbrich
Alexander Weigl
Entwicklung eines formalen Fairnessmodells für Datenverkehr MA / PdF Michael Kirsten
Beendete und laufende Projekt- und Abschlussarbeiten
Titel Typ Betreuer Bearbeiter
Spezifikation und Verifikation von Smart Contracts in Hyperledger Fabric MA Michael Kirsten
Mihai Herda
Jonas Schiffl
Comparing Deductive Program Verification of Graph Data Structures BA Michael Kirsten
Mattias Ulbrich
Jelle Kübler
A Component-Based Approach to the Property-Oriented Design of Voting Rules MA / PdF Michael Kirsten Karsten Diekhoff,
Jonas Krämer
Ownership Types and Dynamic Frames MA / PdF Mattias Ulbrich Wolfram Pfeiffer
Probablistische Beweis-Analyse mit KeY MA Mattias Ulbrich
Mihai Herda
Stefan Kobischke
Produkt-Programme in Java für effiziente relationale Verifikation BA Michael Kirsten
Mattias Ulbrich
Pascal Gabriel
JML-Java Parser BA Alexander Weigl
Flexible Term and Formula Matching BA Sarah Grebing
Exploration of Failed Proof Attempts BA Sarah Grebing Thomas Trapp
Modular Verification of JML Contracts Using Bounded Model Checking MA Mattias Ulbrich
Michael Kirsten
Jonas Klamroth
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
Evaluation der Proof-Script-Sprache für KeY BA Sarah Grebing
Mattias Ulbrich
An Thuy Tien Luong
Automatic Logic-Based Margin Computation for Efficient Election Audits BA Michael Kirsten Larissa Löw
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
Hybrid Systems Verification:
Autonome Navigation von mobilen Robotern
BA Bernhard Beckert David Vogelbacher
Effiziente Verifikation von Informationssicherheit BA Daniel Grahl Fabian Ruch
Formale Verifikation objektorientierter Software für Produktionsanlagen PdF Alexander Weigl
Mattias Ulbrich
Augusto Modanese
Model Generation SA / BA / MA / DA Christoph Gladisch
Verification-based Test Generation BA / SA / MA / DA Christoph Gladisch
Nichtinterferenz in relationalen Datenbanksystemen PdF Simon Greiner
Combining Graph-Based and Deductive Information-Flow Analysis for Proving Non-Interference PdF Mihai Herda
Michael Kirsten
Marko Kleine Büning
MA = Masterarbeit, BA = Bachelorarbeit, DA = Diplomarbeit, SA = Studienarbeit, PdF = Praxis der Forschung