Supervised Theses
Titles Status Student Supervisor(s)
Ghostbusting JML with CATs (opens in new tab) ongoing Marco Scaletta
Choreographic Language Extension for Markov Chain Generation (opens in new tab) ongoing Jasmin Türker Adele Veschetti
DSL für Produktlinien von Benutzeroberflächen (opens in new tab) 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 (opens in new tab) 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 (opens in new tab) 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 (opens in new tab) finished Martina Kettenbach Eduard Kamburjan
Active Object Languages for Railway Modeling (opens in new tab) finished Fabian Wagner Eduard Kamburjan
Comparing ABS and B on Real World Specifications (opens in new tab) finished Chunyuan Yu Eduard Kamburjan
Industrielle Evaluation des Symbolic Execution Debuggers (opens in new tab) finished Lukas Becker Richard Bubel
Algorithmic Debugging with Symbolic Execution Trees (opens in new tab) 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 (opens in new tab) 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 (opens in new tab) 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 (opens in new tab) 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