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

Involvierte Forschungsprojekte: COMSOC, KASTEL

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
Anpassung von Open-Source-Software für den Schulunterricht Mattias Ulbrich
Wartung und Weiterentwicklung von KeY Mattias Ulbrich
Re-Implementation of Concurrent Proof Delegation Jonas Schiffl
Mattias Ulbrich
Offene Projekt- und Abschlussarbeiten
Titel Typ Betreuer/in
Real-time Specification with Contract Automata MA Alexander Weigl
Java Byte-Code Verifikation mit KeY BA Alexander Weigl
Verifikation von Java-Programmen mit Datenbank-Anbindung MA / BA Mattias Ulbrich
Modular Verification of Neural Networks PdF Samuel Teuber
Philipp Kern
Proof Certificates for Neural Network Retraining PdF Samuel Teuber
Philipp Kern
Specification Mining of Contract Automata PdF Alexander Weigl
Java-Spezifikationen mit eingebetteten Beweisen MA Mattias Ulbrich
Wolfram Pfeifer
Modeling and Verification of Smart Contracts BA / MA / HiWi Jonas Schiffl
Beweisbares Vergessen von Information in interaktiven System MA / PdF Alexander Weigl
Verification of Important Data Structures of the JDK BA Mattias Ulbrich
Bounded Verification of Quantum Programs PdF Jonas Klamroth
Dynamisches Prüfen von Fairness-Eigenschaften mit Hilfe von Laufzeitmonitoren PdF Jonas Klamroth
Mattias Ulbrich
Michael Kirsten
Verifying the Hagrid Key-Server with JJBMC BA / MA Mattias Ulbrich
Jonas Klamroth
Verify Your Favourite Voting Rule BA / MA Michael Kirsten
Automated Correct Algorithm Transformation into Map Reduce MA Mattias Ulbrich
Bislicing – Slicing for Relational Verification MA / PdF Mattias Ulbrich
Michael Kirsten
Semantische Datenminimierung PdF Alexander Weigl
Florian Lanzinger
Modellierung von Angriffen für quantitative Sicherheitsanalysen MA Florian Lanzinger
Modelling Smart Contracts as Petri Nets for Verification BA/ MA Jonas Schiffl
Closing the Gap between Models and Programs MA / PdF Florian Lanzinger
Beendete und laufende Projekt- und Abschlussarbeiten
Titel Typ Betreuer/in
Vorverarbeitung durch Dimensionsreduktion für die Verifikation von neuronalen Netzwerken BA Samuel Teuber
Philipp Kern
Judging in Competitive Dancing: Formal Verification of the Skating System BA Michael Kirsten
Formal Verification of Symmetry Properties in Distance-Rationalizable Voting Rules BA Michael Kirsten
Verified Construction of the Instant-Runoff Voting Rule BA Michael Kirsten
Verified Construction of the Split Cycle Voting Rule BA Michael Kirsten
An Automated Approach to Generating Card-Based Cryptographic Protocols BA Michael Kirsten
Verified Efficient Implementation of Modular Voting Rules Using Stepwise Refinement in Isabelle/HOL MA Michael Kirsten
Combining Bisimulation and Predicate Inference for Equivalence Proofs MA / PdF Mattias Ulbrich
Generierung von effektiven Testfällen mithilfe von Software-Differenzen PdF Alexander Weigl
"Proof-Slicing" für KeY-Beweise BA Wolfram Pfeifer
Maschinelle Verifikation von Fairness-Eigenschaften mit Hilfe formaler Informationsflussanalyse PdF Michael Kirsten
Jonas Klamroth
Mattias Ulbrich
Distance Rationalization for Modular Construction of Verified Voting Rules BA Michael Kirsten
Algebraische Datentypen in KeY BA / MA Alexander Weigl
Wolfram Pfeifer
Compositional Verification of Social Choice Properties for Single Transferable Vote Using an Interactive Theorem Prover BA Michael Kirsten
Formal Verification of Scoring-based Voting Rules Using Composable Modules BA Michael Kirsten
Bounded Verification of Fairness Properties for Seat Apportionment Methods BA Michael Kirsten
Formal Verification of Strategic Stability Measures for Scoring Rules Using Iterative Voting BA Michael Kirsten
Automated Verification and Generation of Voting Rules Using Composable Modules 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
Extracting Specifications for KeY PdF Mattias Ulbrich
Applying Software Bounded Model Checking to the Australian Voting Method BA Michael Kirsten
Using System Dependence Graphs for the Automatic Generation of Frame Conditions BA Mihai Herda
Michael Kirsten
Formal Verification of Condorcet Voting Rules Using Composable Modules BA Michael Kirsten
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
Verification of Efficient Arithmetic Operations BA Mattias Ulbrich
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
Exploration of Failed Proof Attempts BA Sarah Grebing
Flexible Term and Formula Matching BA Sarah Grebing
Modular Verification of JML Contracts Using Bounded Model Checking MA Mattias Ulbrich
Michael Kirsten
JML-Java Parser BA Alexander Weigl
Effizienter Umgang mit Zeitkonstanten in der Verifikation reaktiver Systeme MA Mattias Ulbrich
Alexander Weigl
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
Relational Verification of Smart Contracts MA / PdF Jonas Schiffl
Abhängige Eigenschaftstypen in Java BA Florian Lanzinger
Methode zur Datenminimierung mittels syntaktischer Programmpartitionierung BA Florian Lanzinger
Mutability for Property Types in Java MA Florian Lanzinger
Verifizierte Datentypen für Solidity MA / PdF Jonas Schiffl
Neue Interaktionsideen für KeY MA / PdF Wolfram Pfeifer
LiquidRust: Refinement Types for Imperative Languages with Ownership MA Florian Lanzinger
A Translation Layer for Information Flow Verification Systems: Bridging Type Systems with Theorem Prover BA Florian Lanzinger
Effiziente Verifikation von Informationssicherheit BA Daniel Grahl
Hybrid Systems Verification:
Autonome Navigation von mobilen Robotern
BA Bernhard Beckert
Runtime Verification für KI-basierte Systeme PdF Jonas Klamroth
Model Generation SA / BA / MA / DA Christoph Gladisch
Combining Graph-Based and Deductive Information-Flow Analysis for Proving Non-Interference PdF Mihai Herda
Michael Kirsten
Formale Verifikation objektorientierter Software für Produktionsanlagen PdF Alexander Weigl
Mattias Ulbrich
Nichtinterferenz in relationalen Datenbanksystemen PdF Simon Greiner
Rekonstruktion von SMT-Lib-Beweisen innerhalb von KeY MA Mattias Ulbrich
Jonas Schiffl
Quantifizierte Sicherheitsausagen mit Probabilistischen Model-Checker BA Jonas Schiffl
Alexander Weigl
Relational Social-Choice Properties for Secure and Scalable Consensus in the Blockchain PdF Michael Kirsten
Using Machine Learning to Improve Strategy Selection in KeY PdF Mattias Ulbrich
Verification-based Test Generation BA / SA / MA / DA Christoph Gladisch
MA = Masterarbeit, BA = Bachelorarbeit, DA = Diplomarbeit, SA = Studienarbeit, PdF = Praxis der Forschung