## Background

One branch of theoretical computer science is the analysis of algorithms, protocols, hardware circuits and software. We want to analyse a system such as a piece of software or a hardware circuit for desirable properties, or to automatically generate systems with desirable properties. Examples of properties are functional correctness, the absence of forbidden states or deadlocks, or reactivity properties such as that a system is responsive.

Many of these questions just boil down to running algorithms on graphs. For example, to check whether some system fulfills a reactivity property specified in LTL, we would simply construct an automaton such that if it has an accepting run, this accepting run proves that the system is not correct. That is, if the language of the automaton is empty, then the system is correct.

Of course, this is only the beginning because if this was all there is to it, then there would not be much research to do. The **core challenge** in this area is called state space explosion: in order to analyse a system, we usually need to consider exponentially or even double exponentially many different situations. This motivates a lot of research into new algorithms to reduce the number of different situations, often by inventing tricks to analyse similar states simultaneously, or by limiting a system to only "relevant" runs, and abstracting away from runs that don't seem relevant. We are constantly trying to find new tricks to push the limits of what we can compute efficiently.

In the formal methods and tools group at the UT, we work with many techniques including binary decision diagrams and parity games. However, we are also interested in studying abstraction techniques such as IC3, guided refinement, partial order reduction, and so forth. Our other goal is to ensure high performance of algorithms, by smart engineering/coding. There are competitions between scientists and it would be nice if we can win them by using smart algorithms that are fast!

### Other topics

Also open ideas for high performance algorithms / data structures are welcome. We have a focus on efficient implementations and empirical evaluation of algorithms.

#### Prerequisites

- Programming experience recommended
- An affinity with algorithms and logical reasoning

#### Related Modules in the Bachelor TCS

- Discrete Structures and Algorithms (automata and graph algorithms)
- Software Systems (implementing software)

## Available Project Proposals

If you are interested in the general topic of **Systems Analysis**, or if have your own project idea related to the topic, please contact us directly. Alternatively, you can also work on one of the following concrete project proposals: