Theses

The following is a brief summary of the topic areas in which we offer project work and theses. We offer (almost) always current, specific topics for theses within the listed areas. You will also find a selection of specific project and thesis topics at the bottom of this page. If you are interested in one of the topics or topic areas or if you are interested in a position as a student assistant ("HiWi") in these areas, please make an appointment with one of our employees by email.

Topic Areas

If none of the topic areas listed below appeal to you, please speak to one of our employees about other topics. The same applies if you have your own ideas for topics.

Case Studies

We want to conduct as many case studies as possible to evaluate and advance our approaches. Interesting case at the moment include:

  • The Java Collection Framework
  • Functional properties of e-voting systems
  • Verification of (abstract) algorithms, e.g., graph traversal
  • THe verification of published "verification challenges"

Contact person: Mattias Ulbrich

Involved research projects: KeY project

Verification Approaches

In verification, the question of which memory areas may be modified by a program is of central importance. We are looking for a Master's student to work on a project or thesis on different approaches and compare their possibilities (expressiveness, applicability, etc.).

Contact person: Mattias Ulbrich

Involved research projects: KeY project

Fairness of Social-Choice Mechanisms

Social choice mechanisms are algorithms for solving collective decision-making problems, such as political elections or the fair distribution of resources (e.g., data traffic on the internet). For these matters, legal texts make requirements such as "Every vote is equal" or "My data should not be disadvantaged."

But how can it be proven that the voting or routing procedures really fulfill these requirements? Is it possible that the requirements cannot be met by any method? We are looking for motivated Bachelor's and Master's students to formalize corresponding requirements and develop approaches for formally verifying their impossibility or correctness with respect to algorithms, as well as to analyze concrete case studies.

We recommend an illustrative video by the University of Amsterdam to motivate the topic in the context of voting rules.

Contact person: Michael Kirsten

Involved research projects: COMSOC, KASTEL

Verification for Industrial Plants

In the age of Industry 4.0, industrial plants are becoming increasingly complex. Nevertheless, they must guarantee safety and security aspects. This is where we use formal verification to guarantee these properties. We research regression verification to ensure properties across the evolution of software, and we also investigate security attacks on production systems.
For both aspects, we are looking for motivated Bachelor's or Master's students to work on the relevant topics.

Contact person: Alexander Weigl

Involved research projects: IMPROVE APS, KASTEL

Thesis Suggestions

In addition to the above topic areas, the theses and projects listed below are also available.
If none of the topics listed below appeal to you, please feel free to contact us with your ideas (preferably – but not exclusively – within the scope of the topic areas above or the research interests of the respective employees).

Open HiWi Positions
Title Advisor
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
Open Projects and Theses
Title Type Advisor
Fallstudie: Verifikation von Java Controller Software für Cyber-Physische Systeme BA Samuel Teuber
Mattias Ulbrich
Model Consistency, Categorically BA / PdF / MA Romain Pascual
KeY for the verification of Jerboa BA / MA Romain Pascual
Wolfram Pfeifer
Model Slicing PdF Romain Pascual
Mattias Ulbrich
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
Verification of Important Data Structures of the JDK BA Mattias Ulbrich
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
Closing the Gap between Models and Programs MA / PdF Florian Lanzinger
Dependent Types for Java BA / MA Florian Lanzinger
Finished and Ongoing Projects and Theses
Title Type Advisor
Vorverarbeitung durch Dimensionsreduktion für die Verifikation von neuronalen Netzwerken BA Samuel Teuber
Philipp Kern
Proof of Correctness of Homomorphic Voting Rules with Isabelle/HOL BA Michael Kirsten
Program Synthesis from Formal Specifications for Correctness-by-Construction in CorC MA Tabea Bordis
Michael Kirsten
Wolfram Pfeifer
Formalization and Verification of Proportional Representation Voting Systems using Isabelle/HOL: A Study of D’Hondt and Sainte-Laguë Methods MA Michael Kirsten
Transferring Proof Obligations from Program Verification in KeY to Isabelle/⁠HOL BA Wolfram Pfeifer
Michael Kirsten
Traceability and Verifiability of Online Elections at Universities BA Michael Kirsten
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
Real-time Specification with Contract Automata MA Alexander Weigl
Java Byte-Code Verifikation mit KeY BA Alexander Weigl
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
Beweisbares Vergessen von Information in interaktiven Systemen MA / PdF Alexander Weigl
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
Semantische Datenminimierung PdF Alexander Weigl
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
Modellierung von Angriffen für quantitative Sicherheitsanalysen MA Florian Lanzinger
Modelling Smart Contracts as Petri Nets for Verification BA/ MA Jonas Schiffl
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 = Master's Thesis, BA = Bachelor's Thesis, DA = Diploma Thesis, SA = Study Thesis, PdF = Research Project