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.