Prof. Dr. Thomas Zeume

Lebenslauf

Since October 2021: Professorship for Logic and Formal Verification,
Faculty of Computer Science, Ruhr University Bochum

October 2020 - September 2021: Professorship for Logic and Formal
Verification, Faculty of Mathematics, Ruhr University Bochum

April 2020 - September 2020: AssistabtProfessorship for Logic and Formal
Verification, Faculty of Mathematics, Ruhr University Bochum

2009-2020: Scientific assistant, Faculty of Computer Science, TU Dortmund

Forschung

Research interests

My research focuses on theoretical 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 theoretical computer science can be assisted by modern technologies.


Querying dynamic databases

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, Thomas Zeume: Dynamic complexity: recent updates. SIGLOG News 3(2): 30-52 (2016)
- Thomas Zeume. Small Dynamic Complexity Classes. PhD thesis. 2015.
- Slides: Thomas Zeume. An Update on Dynamic Complexity. ICDT 2018
- Thomas Schwentick, Nils Vortmeier, Thomas Zeume. Sketches of Dynamic Complexity. SIGMOD Record, 2020


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 custom logics 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:
- Thomas Schwentick and Thomas Zeume: Two-Variable Logic with Two Order Relations. Logical Methods in Computer Science. 2012.
- Thomas Zeume and Frederik Harwath: Order-Invariance of Two-Variable Logic is Decidable. LICS 2016. (Extended version)
- Ahmet Kara, Thomas Schwentick, and Thomas Zeume: Temporal Logics on Words with Multiple Data Values. FSTTCS 2010: 481-492 (Extended version)
- Szymon Toruńczyk, Thomas Zeume. Register Automata with Extrema Constraints, and an Application to Two-Variable Logic. LICS 2020.


Web-supported teaching in theoretical computer science

Courses on theoretical 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 theoretical computer science education can benefit from modern technologies and student-centered teaching methods.

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 develop the web-based teaching support system Iltis for theoretical computer science courses. A prototypical system for logic-related content is already available.

Try it: An interactive logic course

Selected articles:
- Gaetano Geck, Artur Ljulin, Sebastian Peter, Jonas Schmidt, Fabian Vehlken, Thomas Zeume. Introduction to Iltis: An Interactive, Web-Based System for Teaching Logic. To be presented at ITiCSE 2018.
- Gaetano Geck, Christine Quenkert, Marko Schmellenkamp, Jonas Schmidt, Felix Tschirbs, Fabian Vehlken, Thomas Zeume. Iltis: Teaching Logic in the Web. 2021. (unpublished)

Lehrveranstaltungen

150262 : Komplexitätstheorie

150324 : Model Checking

n.n. : Formale Verifikation

n.n. : Formal Verification

150345 : Logik in der Informatik

150262 : Komplexitätstheorie

150324 : Model Checking

Veröffentlichungen