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

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.

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
Dynamisches Prüfen von Fairness-Eigenschaften mit Hilfe von Laufzeitmonitoren PdF Jonas Klamroth
Mattias Ulbrich
Michael Kirsten
Bounded Verification of Quantum Programs PdF Jonas Klamroth
Maschinelle Verifikation von Fairness-Eigenschaften mit Hilfe formaler Informationsflussanalyse PdF Michael Kirsten
Jonas Klamroth
Mattias Ulbrich
Algebraische Datentypen in KeY BA / MA Alexander Weigl
Compiling KeY Sequents to Why3 MA Lionel Blatter
Verifying the Hagrid Key-Server with JJBMC BA / MA Mattias Ulbrich
Jonas Klamroth
Extracting Specifications for KeY PdF Mattias Ulbrich
Verification of Efficient Arithmetic Operations BA Mattias Ulbrich
Automated Correct Algorithm Transformation into Map Reduce MA Mattias Ulbrich
Bislicing – Slicing for Relational Verification MA / PdF Mattias Ulbrich
Mihai Herda
Relational Verification of Smart Contracts MA / PdF Jonas Schiffl
Runtime Verification für KI-basierte Systeme PdF Jonas Klamroth
Ermittlung von Zuverlässigkeitsmaßen durch unvollständige Verifikation PdF Florian Lanzinger
Implementing an Ideal Ledger Functionality MA / PdF Jonas Schiffl
Beendete und laufende Projekt- und Abschlussarbeiten
Titel Typ Betreuer/in
Verify Your Favourite Voting Rule BA / MA Michael Kirsten
Erweiterung der Theorie für Finale Felder in KeY BA Mattias Ulbrich
Alexander Weigl
Specification Inference for Floating Point Programs MA / PdF Mattias Ulbrich
Entwicklung eines formalen Fairnessmodells für Datenverkehr BA / 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
Using SDGs to Generate Frame Conditions BA Mihai Herda
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
Test Coverage of Generalised Test Tables BA Alexander Weigl
Semantics of Sequential Function Charts BA Alexander Weigl
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
JML-Java Parser BA Alexander Weigl
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
Modular Verification of JML Contracts Using Bounded Model Checking MA Mattias Ulbrich
Michael Kirsten
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
Verifikation von Dafny-Programmen DA Daniel Grahl
Verifiziert sicherer Informationsfluss mit Events BA 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
Abhängige Eigenschaftstypen in Java BA Florian Lanzinger
Methode zur Datenminimierung mittels syntaktischer Programmpartitionierung BA Florian Lanzinger
Model Generation SA / BA / MA / DA Christoph Gladisch
Using Machine Learning to Improve Strategy Selection in KeY PdF Mattias Ulbrich
Hybrid Systems Verification:
Autonome Navigation von mobilen Robotern
BA Bernhard Beckert
Formale Verifikation objektorientierter Software für Produktionsanlagen PdF Alexander Weigl
Mattias Ulbrich
Mutability for Property Types in Java MA Florian Lanzinger
Relational Social-Choice Properties for Secure and Scalable Consensus in the Blockchain PdF Michael Kirsten
Quantifizierte Sicherheitsausagen mit Probabilistischen Model-Checker BA Jonas Schiffl
Alexander Weigl
Rekonstruktion von SMT-Lib-Beweisen innerhalb von KeY MA Mattias Ulbrich
Jonas Schiffl
Effiziente Verifikation von Informationssicherheit BA Daniel Grahl
Nichtinterferenz in relationalen Datenbanksystemen PdF Simon Greiner
MA = Masterarbeit, BA = Bachelorarbeit, DA = Diplomarbeit, SA = Studienarbeit, PdF = Praxis der Forschung