« February 2017 »
You are here: Home Teaching Student Projects and Thesis Topics Finished
Document Actions


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.

[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.
[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. 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.
[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] Reducing the Size of Büchi Automata
We examine and implement an algorithm that reduces the size of Büchi Automata.
[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.
[B.Sc. Project] On-line Simplificaton of Formulas
Implement an simplification algorithm for formulas.
[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...
[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] 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...
[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.
[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.
[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...
Personal tools