We understand Automated Reasoning as the algorithmic exploration of a formal rule set in order to deduce formally precise properties. The many use cases of automated reasoning include electronic hardware design, mathematical theorem proving, and verifying the security, correctness, and fairness of critical systems.

Our aim is to study and advance the generic toolbox at the core of automated reasoning with a distinct focus on parallel and distributed computing. Notable examples for such generic tools include propositional satisfiability (SAT) solving, Satisfiability Modulo Theories (SMT), Bounded Model Checking (BMC), combinatorial optimization (e.g., MaxSAT), and automated planning and scheduling.

Scalability in the context of our research usually encompasses the ability of a tool or method to make graceful and efficient use of increasing amounts of computational resources (e.g., CPUs or cores). In addition, scalability can also be understood in the sense of handling increasingly large and complex inputs.

On a methodological level, we adhere to the principles of Algorithm Engineering, which aims to bridge theory and practice by integrating realistic models, theoretical considerations, practical implementations, and experiments on real-world inputs.

As such, put succinctly, we are conducting research in the intersection of algorithm engineering, parallel computing, and formal methods.