## Prof. Dr. Thomas Zeume

### Logic and Formal Verification

### Contact

E-Mail: thomas.zeume@rub.de

Tel.: +49(0) 234 32-19609

Room: MC 1.65

### Consultation hours

By arrangement

### Vita

### Teaching

since October 2020

April 2020 – October 2020

2015

2004 – 2009

Professorship for Logic and Formal Verification

Faculty of Mathematics & Center of Computer Science, RUB

Assistant Professorship for Logic and Formal Verification

Faculty of Mathematics & Center of Computer Science, RUB

Doctorate in Theoretical Computer Science

TU Dortmund

Computer Science Studies

Leibniz-Universität Hannover

- Logic in computer science
- Formal verification
- Complexity theory
- Automata theory

### Research interests

My research interests lie at the interface of mathematics and computer science. My research focuses on the application of logical and complexity-theoretic methods to computer science scenarios, in particular database theory and verification.

##### 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. One of the main goals in this area is to develop a theory for classifying queries in terms of the amount of resources needed to evaluate them dynamically.

My research investigates (a) methods for determining the set of resources needed to sustain queries in this dynamic context, and (b) 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

##### Logic 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 contributed to the design of a navigational logic, DataLTL, that allows for specifying complex properties of systems with many processes, and whose basic reasoning tasks remain decidable. For another basic specification language, the two-variable fragment of predicate logic, we study the complexity of reasoning tasks for many variants and were able to give a classification of their computational complexity

*Selected papers*

- 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)

##### A web-based system for learning logic

A typical application of logic in computer science is to model a real-world scenario, formulate formulas expressing knowledge about the scenario, and derive new knowledge through logical reasoning. While there is no shortage of software for logic, a closer look reveals that there is almost no current intuitive software system to support student learning for such basic instructional goals.

Our goal is to build such an interactive, web-based system that supports tasks for traditional logic (propositional logic, modal logic, and predicate logic), as well as more domain-specific logic used for verification and database query tasks.

*Try it: *Logic Web Tutorial

**Introduction to the System: **

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.

### Publications

Here you can find an up-to-date list of my publications.

##### Journal Articles

- Samir Datta, Anish Mukherjee, Thomas Schwentick, Nils Vortmeier, Thomas Zeume: A Strategy for Dynamic Programs: Start over and Muddle through. Logical Methods in Computer Science. 2019.
- (Accepted for publication) Pablo Barceló, Miguel Romero, Thomas Zeume: A More General Theory of Static Approximations for Conjunctive Queries.
- Samir Datta, Raghav Kulkarni, Anish Mukherjee, Thomas Schwentick, Thomas Zeume: Reachability Is in DynFO. J. ACM. 2018 (Final manuscript)
- Thomas Schwentick, Nils Vortmeier, Thomas Zeume: Dynamic Complexity under Definable Changes. ACM Trans. Database Syst. 2018 (Final manuscript)
- Thomas Zeume: The dynamic descriptive complexity of k-clique. Inf. Comput. 256: 9-22. 2017. (Final manuscript)
- Thomas Zeume, Thomas Schwentick: Dynamic conjunctive queries. J. Comput. Syst. Sci. 88: 3-26. 2017. (Final manuscript)
- Thomas Zeume and Thomas Schwentick: On the quantifier-free dynamic complexity of Reachability. Information and Computation. 2015.
- Thomas Schwentick and Thomas Zeume: Two-Variable Logic with Two Order Relations. Logical Methods in Computer Science. 2012.

##### Books

- Thomas Zeume. Small Dynamic Complexity Classes: An Investigation into Dynamic Descriptive Complexity, volume 10110 of Lecture Notes in Computer Science. Springer, 2017.
Johannes Albrecht, Carsten Brenner, Bilal Gökce, Pascal Malkemper, Jochen Niemeyer, and Thomas Zeume. I Love to Share Knowledge: A personal perspective on academic teaching. Universität Duisburg-Essen, 2017. ISBN: 978-3-940402-09-7.

##### Conference papers

- Jean Christoph Jung, Carsten Lutz, Thomas Zeume: Decidability and Complexity of ALCOIF with Transitive Closure (and More). Description Logics 2019
- Samir Datta, Anish Mukherjee, Nils Vortmeier, Thomas Zeume: Reachability and Distances under Multiple Changes. ICALP 2018.
- Gaetano Geck, Artur Ljulin, Sebastian Peter, Jonas Schmidt, Fabian Vehlken, Thomas Zeume. Introduction to Iltis: An Interactice, Web-Based System for Teaching Logic. ITiCSE 2018.
- Pablo Barceló, Miguel Romero, Thomas Zeume: A More General Theory of Static Approximations for Conjunctive Queries. ICDT 2018.
- Cynthia Taylor, Jaime Spacco, David P. Bunde, Zack Butler, Heather Bort, Christopher Lynnly Hovey, Francesco Maiorana, Thomas Zeume: Propagating the adoption of CS educational innovations. ITiCSE (Companion) 2018.
- Samir Datta, Anish Mukherjee, Thomas Schwentick, Nils Vortmeier, Thomas Zeume: A Strategy for Dynamic Programs: Start over and Muddle Through. ICALP 2017.
- Thomas Schwentick, Nils Vortmeier, Thomas Zeume: Dynamic Complexity under Definable Changes. ICDT 2017.
- Thomas Zeume and Frederik Harwath: Order-Invariance of Two-Variable Logic is Decidable. LICS 2016. (Extended version)
- Thomas Schwentick, Nils Vortmeier, and Thomas Zeume: Static Analysis for Logic-Based Dynamic Programs. CSL 2015. (Extended version)
- Samir Datta, Raghav Kulkarni, Anish Mukherjee, Thomas Schwentick, and Thomas Zeume: Reachability is in DynFO. ICALP 2015. (Extended version)
- Thomas Zeume: The Dynamic Descriptive Complexity of k-Clique. MFCS 2014.
- Thomas Zeume and Thomas Schwentick: Dynamic Conjunctive Queries. ICDT 2014.
- Amaldev Manuel and Thomas Zeume: Two-Variable Logic on 2-Dimensional Structures. CSL 2013.
- Thomas Zeume and Thomas Schwentick: On the quantifier-free dynamic complexity of Reachability. MFCS 2013. (Extended version)
- Ahmet Kara, Thomas Schwentick, and Thomas Zeume: Temporal Logics on Words with Multiple Data Values. FSTTCS 2010. (Temporal Logics on Words with Multiple Data Values)
- Thomas Schwentick and Thomas Zeume: Temporal Logics on Words with Multiple Data Values). CSL 2010.
- Jarkko Kari, Pascal Vanier, and Thomas Zeume: Temporal Logics on Words with Multiple Data Values. MFCS 2009.

##### Others

- (Poster) Gaetano Geck, Artur Ljulin, Jonas Haldimann, Johannes May, Jonas Schmidt, Marko Schmellenkamp, Daniel Sonnabend, Felix Tschirbs, Fabian Vehlken, Thomas Zeume: Teaching Logic with Iltis: an Interactive, Web-Based System. ITiCSE 2019: 307
- Thomas Schwentick, Thomas Zeume: Dynamic complexity: recent updates. SIGLOG News 3(2): 30-52 (2016)
- PhD thesis: Small Dynamic Complexity Classes. 2015. Reviewers: Erich Grädel, Thomas Schwentick
- Diploma thesis: Small Dynamic Complexity Classes. 2009. Examiners: Jarkko Kari, Heribert Vollmer.