Prof. Dr. Thomas Zeume
Logic and formal verification
Professor / Chair management

Curriculum Vitae
- 2020 – : Professor for Logic and Formal Verification, Ruhr University Bochum
- 2009-2020: Scientific assistant, Faculty of Computer Science, TU Dortmund
Teaching
- Logic in computer science
- Theoretical computer science
- Computational complexity theory
- Highlights of theoretical computer science
Research
Research interests
My research focuses on formal foundations of computer science, in particular on computational logic and its applications in database theory, complexity theory and formal verification. In my research, I also explore how the teaching of formal foundations of computer science can be assisted by educational technologies.
Querying dynamic data bases
Extracting information from vast amounts of data that are frequently updated is a major challenge in many disciplines. Dynamic complexity theory studies the theoretical foundations of logical query languages for databases that are subject to frequent changes. A major goal of this area is to develop a theory for classifying queries in terms of the number of resources needed to evaluate them dynamically.
In my research, I (a) develop methods for determining the number of resources needed to update query results in this dynamic context, and (b) investigate the structure of small dynamic complexity classes and their relationship to traditional static complexity classes.
A good start to the area:
- Thomas Schwentick, Nils Vortmeier, Thomas Zeume: Sketches of Dynamic Complexity. SIGMOD Record, 2020.
- Slides: Thomas Zeume. An Update on Dynamic Complexity. Tutorial at ICDT 2018.
- Thomas Schwentick, Thomas Zeume: Dynamic complexity: recent updates. SIGLOG News, 2016.
- Thomas Zeume: Small Dynamic Complexity Classes. PhD thesis. 2015.
Selected articles:
- Samir Datta, Raghav Kulkarni, Anish Mukherjee, Thomas Schwentick, Thomas Zeume. Reachability Is in DynFO. Journal of the ACM, 2018.
- Thomas Schwentick, Nils Vortmeier, Thomas Zeume. Dynamic Complexity Under Definable Changes. ACM Transactions on Database Systems 2018.
Foundations of logics for specification and verification
Automated verification of software and hardware is an important task. Often intended properties of a system are specified by logical formalisms that navigate along traces of the system. Similar formalisms are the basis for query languages for extracting information from XML documents and graph databases.
In my research, I explore logical systems with respect to their applicability for such tasks. I design customlogics and explore their basic algorithmic properties for reasoning tasks as well as their expressivity. One focus has been on extensions of the two-variable fragment of predicate logic, where we obtained a classification of the computational complexity of the satisfiability problem.
Selected articles:
- Corentin Barloy, Michaël Cadilhac, Charles Paperman, Thomas Zeume. The Regular Languages of First-Order Logic with One Alternation. LICS 2022.
- Szymon Toruńczyk, Thomas Zeume: Register Automata with Extrema Constraints, and an Application to Two-Variable Logic. LICS 2020
- Thomas Zeume and Frederik Harwath: Order-Invariance of Two-Variable Logic is Decidable. LICS 2016. (Extended version)
- Thomas Schwentick and Thomas Zeume: Two-Variable Logic with Two Order Relations. Logical Methods in Computer Science. 2012.
Educational technologies for formal foundations of computer science
Courses on formal foundations of computer science are typically among the hardest for computer science students. Improving motivation and understanding in these courses is therefore an important goal. For increasing learning outcomes in STEM disciplines (science, technology, engineering, and mathematics) the National Research Council of the US advocates, among others, to “Make classrooms interactive, both to engage students and to provide dynamic feedback in situ;” and to “Leverage technologies to make the most effective use of students’ time, shifting from information delivery to sense-making and practice in class.”. This raises the question of how education of formal foundations can benefit from modern educational technologies.
I am convinced that we, as computer scientists, need to address this challenge in order to provide our students with the best learning opportunities. In our group we combine insights from formal foundations and from CS education research to built the state-of-the-art educational support system Iltis.
Try it: Learning Formal Foundations of Computer Science with Iltis
A good start to the area:
- Marko Schmellenkamp, Fabian Vehlken, and Thomas Zeume. Teaching formal foundations of computer science with Iltis. Bulletin of the EATCS 2024.
- Slides: Thomas Zeume. Iltis: Learning Logic on the Web. 2025
Selected articles:
- Tristan Kneisel, Elias Radtke, Marko Schmellenkamp, Fabian Vehlken, Thomas Zeume:
Tool-Assisted Learning of Computational Reductions. Technical Symposium on
Computer Science Education (SIGCSE TS) 2025. - Tristan Kneisel, Fabian Vehlken and Thomas Zeume. Logical Modelling in CS
education: Bridging the Natural Language Gap. To appear at the International
Conference on Artificial Intelligence in Education (AIED) 2025. - Marko Schmellenkamp, Alexandra Latys, and Thomas Zeume. Discovering and quantifying misconceptions in formal methods using intelligent tutoring systems. Technical Symposium on Computer Science Education (SIGCSE TS) 2023.
Publications
Here you can find an up-to-date list of my publications.