You are here: Home Teaching Student Projects and … Finished

Finished

Selection of student projects and thesis topics that have already been finished. If you find one of the topics interesting please ask the tutor about similar or follow up projects/theses.
[Varies] Complementation of Buchi Automata
How can we complement Büchi automata? Analyze existing algorithms and design an implementation of such an algorithm in out automata library.
[B.Sc. Project] IK, Modelling the Work Activity of the Energy Systems Department, 2013.
Elicitation and documentation of service group processes, relationships between organisational levels; and roles, rights, and permissions in the Energy Systems department.
[M.Sc. Thesis] KF, Extending the Reduction of Quasi-equal Clocks in Networks of Timed Automata, 2013.
Elaboration and evaluation of a new approach for the reduction of quasi-equal clocks in networks of timed automata.
[Varies] Minimization of Nested Word Automata
Examine minimization algorithms for different kinds of automata. Develop a minimization algorithm for a variant of nested word automata. Implement your algorithm in our automaton tool.
[B.Sc. Thesis] Minimization of Finite Automata
We implement several minimization algorithms for finite automata in our framework and compare time and memory consumption. Additionally, we want to solve the question whether parallelization can improve the existing approaches.
[B.Sc. Project] Petri Net Unfolder
Use a Petri net unfolding algorithm to design an emptiness test for the Petri net acceptors in our automata library.
[M.Sc. Laboratory] Reducing the Size of Büchi Automata
We examine and implement an algorithm that reduces the size of Büchi Automata.
[M.Sc. Thesis] SPI-Bus Protocol for Embedded Systems
Development and implementation of a verified transport layer protocol for a given SPI bus hardware.
[M.Sc. Laboratory] A Study of Software Model Checkers based on Interpolation
We compare techniques of some existing software model checkers, identify differences and commonalities and check if we can present the techniques in a unified framework.
[Varies] Synthesis of Ranking Functions
From the halting problem, we know that there is no algorithm that can decide termination for all programs. Here we develop an algorithm that decides termination for some programs. We will develop and analyze templates that can be used to compute ranking functions.
[M.Sc. Laboratory] Synthesis of Ranking Functions for Lasso Programs
From the halting problem, we know that there is no algorithm that can decide termination for all programs. In this project we develop an algorithm can be used to synthesize ranking functions of a certain kind. We will use this algorithm to show termination of all programs which have a ranking function of this kind.
[B.Sc. Thesis] Trace Abstraction for Concurrent Programs via Petri Net Acceptors
Extend the trace abstraction approach to program verification to concurrent programs by using petri net acceptors instead of finite automata.
[M.Sc. Team Project] Ultimate Team Project
Extend the ULTIMATE software model checker to a tool which can verify C code, is integrated in Eclipse CDT and available via a web interface.
[B.Sc. Thesis] Delta Debugger for C programs
Implementation of a general delta debugger for C programs.
[B.Sc. Project] On-line Simplificaton of Formulas
Implement an simplification algorithm for formulas.