Welcome to the Institute for Theoretical Computer Science


We represent theoretical computer science at the Department of Computer Science and Automation at Ilmenau University of Technology. By this we mean in particular algorithms and complexity theory, automata theory and logic in computer science. These focal points are reflected in the courses offered, in the research and in the division of the institute into the subject areas  "Algorithms" and "Automata und Logic".

Institute Director



Jana Berlit


+49 3677 69-2655

🖷 +49 3677 69-1237

⌂  Zusebau, room 1046


Technische Universität Ilmenau

Department of Computer Science and Automation

Institute for Theoretical Computer Science

PO Box 10 05 65

98684 Ilmenau

Technical Administration
Dipl.-Ing. Andreas Krechla


+49 3677 69 – 2787

  Zusebau, room 1049

Detailed information

Groups in the Institute for Theoretical Computer Science

The algorithms group focuses on the development of algorithmic methods and on exploring their inherent limitations.

The two key questions are:

  • In which situations do efficient algorithms exist and what is the structural difference between "easy" and "hard" input instances?
  • What are the strengths and limits of certain algorithmic strategies and solution methods?

The investigated settings include classic decision problems (such as the satisfiability test of propositional logic), counting and enumeration algorithms (determining the number of or generate all solutions) to dynamic algorithms that support efficient update operations.

Concrete fields of application of this research are

  • methods for query optimization and query evaluation on relational and probabilistic databases as well as
  • methods and data structures in the area of SAT and constraint solving.

The research interests of the Automata and Logic group are in the areas of methods for automatic verification of distributed systems and automatic structures. In particular, these investigations use methods from logic and automata theory, and thus belong to the broader area of logic in computer science.

In automatic verification, we try to find a trade-off between the expressiveness of specification languages and their algorithmic controllability. In this context, recently gained theoretical insights on distributed models with finitely many internal states are also investigated, adapted and extended with respect to their practical relevance.

In addition to these systems, the verification of those with infinitely many internal states (which can occur, for example, due to stacks or string variables) is also of interest. An abstract model of these systems are automatic structures. We study these structures from the algorithmic side (Which questions are solvable with which effort?) and from the abstract side (Which model-theoretic properties characterize these structures?).

At the core of (almost) every serious computer science application are clever algorithms that solve the basic tasks required in each case: Managing data so that it can be found quickly based on keys, sorting, finding short paths or cheap connections in networks, finding partial structures such as words in texts or partial patterns in images, routing messages in networks on short paths that are easy to find.

Despite ever faster computers, in many cases good algorithms are needed to cope with the also ever increasing amount of data. The subject of the work of the department are such algorithms.

The parts "Efficient Algorithms" and "Complexity Theory" form two sides of the same coin:

In the area of "Efficient Algorithms" one deals with the maintenance of a large pool of established algorithms, with design strategies and with methods that allow the quantitative prediction of the resource consumption of algorithms. An increasingly important aspect is the relatively new field of "Algorithm Engineering", which focuses on the problems of implementing and controlling the real-world behavior of implemented algorithms, especially with respect to modern computer architectures.

In "complexity theory" one makes investigations to show that certain problems probably cannot be solved efficiently (i.e. fast or in a given amount of memory or with a given communication overhead) - such statements help in the field of algorithm design to decide when it is better to resort to approximate solutions or, foregoing performance guarantees, to heuristics.