Maybe this website is out of date.
Please visit the current version.
University of Konstanz
University of Konstanz
Chair for Software Engineering

Student Topics

Bachelor Projects, Master Projects, Hiwi-Jobs

We are constantly looking for students interested in bachelor or master projects in our group. At the moment, we also have some positions as research assistants (Hiwi-Students) available.

Have a look at some currently available projects or at the completed projects and theses:

Mentor Conversation

Bachelor program documents
Master program documents

Modeling of Embedded (Automotive) Systems

Model-based construction of software has become increasingly important especially for embedded software, e.g. software that runs in cars, airplanes, or small devices. In all of these domains, software quality, i.e. the absence of bugs, is very important. In our research, we aim to improve software quality by proving some properties - like unreachability of certain "error-states" - by means of model checking.

Here are some specific ideas that could be done either as Bachelor Project, Master Project or Hiwi position (25 - 85 hours per month, depending on your time and ambition):

Projects for Students on Bachelor Level


Projects for Students on Master Level

Please note that these are only some suggestions. You are welcome to bring your own ideas for projects in this general setting.

Contact: Florian Leitner-Fischer

Heuristics-Guided Dependability Analysis

Stochastic Model Checking is an automated technique to systems with respect to their performance and dependability which are important aspects of the system quality. However, current stochastic model checking tools do not provide diagnostics and debugging information. This fact constrains their practical use. We are working on this problem in the scope of the DiRePro project funded by the DFG and associated with the Transregional Collaborative Research Center 14 AVACS. We investigate methods to generate diagnostics information for stochastic model checking. We apply heuristic-guided search algorithms, like Best-First Search, to efficiently determine diagnostic traces, also known as failure traces or counterexamples, which carries large amount of probability. The delivered traces are essential tools for diagnostics and debugging. In the course of our work on this topic, a prototype tool called DiPro has been implemented. DiPro is implemented in Java and linked to the stochastic model checkers PRISM developed bei the research group of Prof. Marta Kwiatkowska at the Computing Laboratory of the University of Oxford, UK and to MRMC developed by the Formal Methods & Tools (FMT) group at the University of Twente, The Netherlands and the Software Modeling and Verification (MOVES) group at RWTH Aachen University, Germany under the guidance of Prof. Dr. Ir. Joost-Pieter Katoen.

Features of DiPro:
  1. Directed and undirected search algorithms for exploring the state space of probabilistic models on-the-fly
  2. Generation of diagnostic traces carrying a high amount of probability and counterexamples for probabilistic timed safety propertie
  3. On-the-fly visualization of state space of probabilistic models
  4. Presenting the solution in various formats, e.g. AUT and DOT
DiPro is still under construction and a lot of work should be done to achieve the status of a stable and convenient tool. Within the scope of the development of DiPro we offer Bachelor and Master projects in the following tasks:
  1. Implementation of Interfaces to existing stochastic model checkers like MRMC
  2. Integration of DiPro into PRISM Model Checker
  3. Working on the visualization of state spaces
  4. Modeling of practical case studies in PRISM and analyzing them using DiPro
While Bachelor projects are on the level of development and application, Master projects are supposed to be research oriented involving creativity and autonomous problem solving. Concrete samples for project topics:

On both Bachelor and Master levels the work is performed in agreeable environment. The close collaboration with other team members and the intensive and direct supervision make it easier to come up with creative ideas, to address challenges and to solve problems.
In the case of interest, please contact us per e-mail or phone. We will be happy to talk to you about details in an individual meeting.

Contact: Florian Leitner-Fischer

Quantitative Analysis of Software and Software Architectures

When developing a safety-critical system it is essential to obtain an assessment of different design alternatives.
In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work.
We work on developing methods and tools that bridge the gap between academia and industrial practice.
QuantUM is one of these tools and allows for the quantitative safety analysis of UML models.

Contact: Florian Leitner-Fischer


VIP ist ein systemunabhängiger Editor für die Modellierungssprache V-Promela. V-Promela ist eine visuelle, objektorientierte Erweiterung von Promela zur hierarchischen Modellierung von Architektur und Verhalten von verteilten, nachrichten-basierten reaktiven Systemen. Auf Bachelor-Level bieten wir Projektthemen in den folgenden Aufgabenbereichen:
Contact: Florian Leitner-Fischer

Current/Completed Projects and Theses

This is a (incomplete) list of current and completed projects and theses.

Projects for Students on Bachelor Level

Projects for Students on Master Level