| Titles | Status | Student | Supervisor(s) | 
|---|---|---|---|
| Ghostbusting JML with CATs (wird in neuem Tab geöffnet) | ongoing | Marco Scaletta | |
| Choreographic Language Extension for Markov Chain Generation (wird in neuem Tab geöffnet) | ongoing | Jasmin Türker | Adele Veschetti | 
| DSL für Produktlinien von Benutzeroberflächen (wird in neuem Tab geöffnet) | finished | Gregor Heß | Richard Bubel Reiner Hähnle | 
| Efficient Modular Specification and Reasoning using Dynamic Frames | finished | Marc Arnold | Richard Bubel | 
| Effective and Efficient Reasoning about (Finite) Sets | finished | Niklas Alt | Richard Bubel | 
| Variable Modules | finished | Eduard Kamburjan | |
| Concept Formation in Computer Science: Modeling and Programming | finished | Markus Kaltenpoth | Eduard Kamburjan | 
| Makroskopisches Editieren von prototypischen Eisenbahnbetriebsverfahren | finished | Jonas Stromberg | Eduard Kamburjan | 
| Semi-Dynamic Session Types for ABS | finished | Anton Haubner | Eduard Kamburjan | 
| Proof Statistics for KeY | finished | Shivaraj Bheemsha Behere | Richard Bubel | 
| Conflict Based Quantifier Instantiation for the KeY Theorem Prover | finished | Andre Challier | Richard Bubel | 
| Speculated Loop Invariants for Proofs (wird in neuem Tab geöffnet) | finished | Daniel Pöppelmann | Jakob Laenge, Dominic Steinhöfel | 
| Modellierung von Software Produktfamilien im Steuerrecht | finished | Nikolas Asimyadis | Richard Bubel | 
| Symbolic State Debugging of C/LLVM-IR programs (wird in neuem Tab geöffnet) | finished | Sha Teng | Nathan Wasser, Asma H. Tabar, Richard Bubel | 
| Loop Scopes Taclets for KeY | finished | Benedikt Dreher | Dominic Steinhöfel, Nathan Wasser | 
| Formalizing the Concurrency Model of Active Objects in a Linearization Framework | finished | Markus Bommer | Eduard Kamburjan | 
| Performance Evaluation of Selected Abstract Behavioral Specification Language Backends | finished | Awsaf Rahman | Richard Bubel | 
| Hybrid Active Objects with ABS (wird in neuem Tab geöffnet) | finished | Martina Kettenbach | Eduard Kamburjan | 
| Active Object Languages for Railway Modeling (wird in neuem Tab geöffnet) | finished | Fabian Wagner | Eduard Kamburjan | 
| Comparing ABS and B on Real World Specifications (wird in neuem Tab geöffnet) | finished | Chunyuan Yu | Eduard Kamburjan | 
| Industrielle Evaluation des Symbolic Execution Debuggers (wird in neuem Tab geöffnet) | finished | Lukas Becker | Richard Bubel | 
| Algorithmic Debugging with Symbolic Execution Trees (wird in neuem Tab geöffnet) | finished | Peter Schauberger | Martin Hentschel, Richard Bubel | 
| A Formal Model of a Railway Operating Procedure with Moving Blocks and Dynamic Speed Profile | finished | Stefan Dillmann | Eduard Kamburjan, Frederik Düpmeier | 
| Join Block Contracts for a Dynamic Logic Calculus (wird in neuem Tab geöffnet) | finished | Melisa Mendoza | Dominic Scheurer, Richard Bubel | 
| Session Types for ABS | finished | Eduard Kamburjan | Crystal Chang Din, Tzu-Chun Chen | 
| Symbolic Execution on a DAG | finished | Dominic Scheurer | Reiner Hähnle, Nathan Wasser, Richard Bubel | 
| Automatische Analyse von Geschäftsregeln (wird in neuem Tab geöffnet) | finished | Johannes Schramm | Reiner Hähnle, Richard Bubel | 
| Abstract Operation Contracts | finished (won Datenlotsenpreis 2015) | Maria Pelevina | Reiner Hähnle, Richard Bubel | 
| Formalising the Method Contract Rule in COQ | finished | Alexander Fuhs | Richard Bubel | 
| Guided Navigation in Symbolic Execution Trees (wird in neuem Tab geöffnet) | finished | Martin Möller | Reiner Hähnle, Martin Hentschel | 
| Effizientes automatisches Beweismanagement in Eclipse für KeY | finished | Stefan Käsdorf | Reiner Hähnle, Martin Hentschel | 
| Erweiterte Kontrollfunktionen für den Symbolic Execution Debugger | finished | Marco Drebing | Reiner Hähnle, Martin Hentschel | 
| Abstract Modeling of Business Software | finished | Marko Martin | Reiner Hähnle, Richard Bubel | 
| Erkennung von korrumpierten Beweisen auf Basis von DbC-Diagrammen | finished | Jan Erik Keller | Reiner Hähnle, Martin Hentschel | 
| Abstract Object Creation for an Explicit Heap Representation | finished | Eduard Kamburjan | Richard Bubel | 
| Erstellung einer Testmethodologie zur Migration im SAP-Umfeld: Angewandt auf eine Fallstudie mit der Untersuchung zur Praktikabilität der Delta-Orientierten Programmierung | finished | Can Güler | Richard Bubel | 
