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. 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 Mitarbeiter/in ("HiWi") in diesen Bereichen interessiert sind, vereinbaren Sie doch einen Termin mit einem/r unserer Mitarbeiter/innen per E-Mail.

Themengebiete

Sollte Sie keines der im Folgenden ausgeschriebenen Themengebiete ansprechen, sprechen Sie eine/n unserer Mitarbeiter/innen 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 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.

Ansprechperson: Michael Kirsten

Involvierte Forschungsprojekte: COMSOC, 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.

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 aus-schließlich – im Rahmen der Themengebiete oben oder Forschungsinteressen der jeweiligen Mitarbeiterinnen oder Mitarbeiter) auf uns zu.

Offene HiWi-Stellen
Titel Betreuer/in
Weiterentwicklung von DIVE Mattias Ulbrich
Wartung und Weiterentwicklung von KeY Mattias Ulbrich
Anpassung von Open-Source-Software für den Schulunterricht Mattias Ulbrich
Re-Implementation of Concurrent Proof Delegation Jonas Schiffl
Mattias Ulbrich
Offene Projekt- und Abschlussarbeiten
Titel Typ Betreuer/in
Entwicklung eines formalen Fairnessmodells für Datenverkehr MA / PdF Michael Kirsten
Konformanz von Testtabellen mittels Hornklauseln BA / MA Alexander Weigl
Maschinelles Lernen von Invarianten für Regression Verification MA / PdF Alexander Weigl
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
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
Using Machine Learning to Improve Strategy Selection in KeY PdF Mattias Ulbrich
Rekonstruktion von SMT-Lib-Beweisen innerhalb von KeY MA Mattias Ulbrich
Jonas Schiffl
Beendete und laufende Projekt- und Abschlussarbeiten
Titel Typ Betreuer/in
Verify Your Favourite Voting Rule BA / MA Michael Kirsten
Spezifikation und Verifikation von Smart Contracts in Hyperledger Fabric MA Michael Kirsten
Mihai Herda
Comparing Deductive Program Verification of Graph Data Structures BA Michael Kirsten
Mattias Ulbrich
A Component-Based Approach to the Property-Oriented Design of Voting Rules MA / PdF Michael Kirsten
Ownership Types and Dynamic Frames MA / PdF Mattias Ulbrich
Probablistische Beweis-Analyse mit KeY MA Mattias Ulbrich
Mihai Herda
Produkt-Programme in Java für effiziente relationale Verifikation BA Michael Kirsten
Mattias Ulbrich
Modular Verification of JML Contracts Using Bounded Model Checking MA Mattias Ulbrich
Michael Kirsten
Exploration of Failed Proof Attempts BA Sarah Grebing
JML-Java Parser BA Alexander Weigl
Flexible Term and Formula Matching BA Sarah Grebing
A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification BA Michael Kirsten
Mattias Ulbrich
Applying Bounded Verification to the German Seat Distribution Procedure BA Michael Kirsten
Evaluation der Proof-Script-Sprache für KeY BA Sarah Grebing
Mattias Ulbrich
Automatic Logic-Based Margin Computation for Efficient Election Audits BA Michael Kirsten
Applying Relational Techniques for the Deductive Verification of Voting Systems BA Thorsten Bormer
Mattias Ulbrich
Michael Kirsten
Formalisierung von Verhaltensdifferenzen in Automatisierungssoftware BA Mattias Ulbrich
Alexander Weigl
Zustandsfolgenbasierte Programmverifikation SA Daniel Grahl
Verifiziert sicherer Informationsfluss mit Events BA Daniel Grahl
Verifikation von Dafny-Programmen DA Daniel Grahl
Combining Graph-Based and Deductive Information-Flow Analysis for Proving Non-Interference PdF Mihai Herda
Michael Kirsten
Verification-based Test Generation BA / SA / MA / DA Christoph Gladisch
Effiziente Verifikation von Informationssicherheit BA Daniel Grahl
Formale Verifikation objektorientierter Software für Produktionsanlagen PdF Alexander Weigl
Mattias Ulbrich
Model Generation SA / BA / MA / DA Christoph Gladisch
Hybrid Systems Verification:
Autonome Navigation von mobilen Robotern
BA Bernhard Beckert
Nichtinterferenz in relationalen Datenbanksystemen PdF Simon Greiner
MA = Masterarbeit, BA = Bachelorarbeit, DA = Diplomarbeit, SA = Studienarbeit, PdF = Praxis der Forschung