I am an assistant professor at the Formal Methods and Tools group at the University of Twente.
My research is connected to formal verification and synthesis, including the efficient solving of **parity games**, using **binary decision diagrams** in formal methods and **SAT/SMT solving** with **multi-core parallelism**. I like making and improving **usable research tools**.

My PhD thesis was on parallelizing decision diagram algorithms. I implemented the Sylvan multi-core decision diagram package, which supports binary decision diagrams and multi-way (list) decision diagrams with custom leaves (booleans, integers, rational functions, etc), that is, binary and multi-way algebraic decision diagrams. The package is used in several applications, including the model checkers LTSmin, Storm and IscasMC, as well as the symbolic bisimulation minimisation tool SigrefMC.

After my PhD, I worked as a Postdoc in the Formal Models and Verification group of Armin Biere, where I mostly studied parity games. I implemented the Oink parity game solver as a platform for studying different parity game algorithms and with the additional objective of practical performance. Oink is now the state-of-the-art in practical parity game solving. I also implemented the synthesis tool Knor for the SYNTCOMP competition, which accepts as input a parity automaton in the HOA specification language, and constructs as output a Mealy controller as an and-inverter-graph in the AIGER format.

I continue designing algorithms that solve parity games. Hopefully one of these runs in polynomial time. My algorithms mostly use the *tangle attractor* to partition a parity game and its subgames into smaller regions, learning new tangles until winning regions are found.

- Sylvan – A multi-core implementation of decision diagrams.
- Lace – Work-stealing framework in C, similar to Cilk.
- SigrefMC – Symbolic bisimulation minimisation for LTS, CTMC and IMC systems.
- Oink – Library/implementation of various parity game algorithms.
- Knor - Reactive controller synthesis from parity automaton (HOA format) to controller (AIGER format).
- See also my Github repositories

- 2019 [Software science]
**Parity Games**(2.5 EC course in the Computer Science Master)- Four lectures and tutorial/homework to implement algorithms in Python
- Slides of all lectures

- 2019-
**Software Systems**(Module 2 of the Computer Science Bachelor)- In 2019, I was one of the teachers of the Programming line
- I now coordinate the 12 EC Module core and teach the Programming line

- 2020 [Software science]
**Model Checking and Parity Games**(5 EC course in the Computer Science Master) - 2022 [Software science]
**Model Checking and Parity Games**(5 EC course in the Computer Science Master) - 2022
**Data Science & AI: SAT/SMT solving**- I teach a minor part of ``Knowledge Representation and Reasoning’’ of Module 9 of the Computer Science Bachelor, which is about Data Science & Artificial Intelligence
- One lecture and a handful of practical assignments, in total about 0.5 EC.

- 2022
**Programming Paradigms - Logic Programming**(Module 8 of the Computer Science Bachelor)- I teach the Logic Programming strand, which is about 2 weeks of teaching. This consists of three lectures about Prolog, several practicals ran by teaching assistants, and a project.

- 2024 [Software science]
**Model Checking and Parity Games**(5 EC course in the Computer Science Master)

Students (BSc, MSc, etc) are welcome to study questions about parity games, binary decision diagrams, and related topics. I have a number of open questions and assignments available.

Design projects are for students who work in a group to design a piece of software, i.e., Module 11 TCS students.

- A graphical user interface for parity games
- The primary objective is to understand and develop parity game algorithms.
- The GUI should let a user create, load and change parity games.
- The GUI should offer various tools to manipulate vertices of the game and to change the layout.
- Ideally, a GUI should allow pattern-based generation of parity games.
- The GUI should support viewing step-by-step execution of different parity game algorithms.

Topics on parity games:

~~Can you efficiently derive a strategy for the winning player in the fixpoint algorithm?~~

Can you do it using binary decision diagrams?

**Now solved, see this 2019 paper with Bob Rubbens and this 2020 paper with Oebele Lijzenga.**- Implement symbolic FPJ in Knor. Symbolic FPJ was investigated/implemented by Oebele Lijzenga.

*Knor implements FPI with freezing to solve symbolic parity games in a very specific format. How would symbolic FPJ do and possibly other symbolic algorithms?* - Investigating an idea to get smaller strategies by trying to solve only parts of the parity game starting in some initial state.

*The idea is that by increasing the window (how far we allow players to play), the solver might come up with a winning strategy that involves fewer vertices.* - Recently, researchers used Sylvan (my BDD package) to implement symbolic Rabin game solving. Thus I wonder if their symbolic Rabin game solver can be ported to Knor.
- What is the effect of different LTL-to-PG constructions on the size of the final constructed controller?
- What is the effect of different LTL-to-NBA constructions for the performance of LTL model checking in LTSmin?

Related to parallel programming, that is, load balancing by work stealing (my Lace framework):

- Porting my work-stealing queue Lace to either Rust or Java (or C++).

*Lace works very well and with very little overhead in C. How well does it work using other programming languages?* - How do the load balancing frameworks Lace, Cilk, OpenMP and Intel TBB compare?

*While there are already some benchmarks, what lacks is a comprehensive benchmark suite that compares Lace to Cilk and OpenMP and Intel TBB or similar technologies.*

Other topics:

- Try new hash tables like F14 in Sylvan.

*Since my research on this in 2012-2016, there are probably faster hash tables. Sylvan uses a custom hash table based on linear probing, and there is a variant using chaining. For the evaluation, most important is the parallel performance of the hash table. It doesn´t need to be implemented in Sylvan per se, a prototype can be made outside Sylvan.* - Implement BDD hash tables on the GPU using Cuckoo hashing and implement basic BDD operations.
- Scheduling TAs is an interesting computational challenge. Can we use for example modern SAT/SMT solvers, or other tools, to find the best schedule for TAs in Module 2?
- Apply parallel dynamic variable reordering in Sylvan to fault trees.

*One of the applications of BDDs is the analysis of fault trees. Finding a good variable order is a challenge, and dynamic variable reordering using sifting is one of the solutions. We have an implementation in Sylvan, but need to apply it to fault trees.*

Topics on parity games:

- Can you implement Lehtinen’s register games solver without constructing the intermediary safety game?

*See her 2018 paper. First implement the safety game construction of the paper and use it to solve parity games; can we find an algorithm that solves the safety game on-the-fly without constructing it explicitly?* - How can we solve parity games and obtain
**small**strategies?

*For example using incremental parity game solving techniques, starting with the vertices that correspond to the initial state of the input game. Current algorithms implemented in Oink are very fast but may also result in very large strategies, ultimately resulting in large controllers rather than small controllers.* - Find a parity game family that runs in exponential time for two-player distraction-free tangle learning, or for distraction-free tangle learning with recursion.

*The idea is that two-player distraction-free tangle learning***probably**requires exponential time, but I do not yet have an example parity game family for this.

Related to parity games are questions like:

- How do tangles arise the translation of LTL synthesis/model-checking to Parity Games? And how do distractions / nested structures of tangles and distractions arise in these applications?

*The idea here is to investigate encodings from LTL synthesis to parity games, and to investigate how tangles in the parity game correspond with features of the encoding.*

On using binary decision diagrams to solve parity games symbolically:

- Can you implement the “tangle learning” algorithm using binary decision diagrams?

*The challenge is to find a good way to encode tangles using binary decision diagrams.*

On proving properties using a theory prover (like Isabelle):

- Can you prove that the work stealing deque in Lace is correct?

Related to my research on binary decision diagrams (my Sylvan package):

~~How to implement and tune parallel dynamic variable reordering for BDDs in Sylvan?~~- Using a hash table per variable level instead of a single hash table for everything in Sylvan.

- How to use tangle attractors for energy parity games and for mean payoff games?

*This topic is quite open. Energy parity games and mean payoff games are related to parity games; the idea is to investigate whether the tangle learning idea can be reused for these related games.* - Can you solve Rabin games using attractors and tangles?

*Rabin games are an alternative to parity games for applications such as LTL synthesis.*

I am open for collaboration on topics related to parity games, LTL synthesis and binary decision diagrams. If you want to use Sylvan for something that is not currently supported, feel free to contact me.

2021
Remco Abraham, Tom van Dijk and Salomon Sickert, *Almost-Symbolic Synthesis via Delta2-Normalisation for Linear Temporal Logic*, SYNT 2021
pdf
2021
Steven Monteiro, Erikas Sokolovas, Ellen Wittingen, Tom van Dijk and Marieke Huisman, *IntelliJML: a JML plugin for IntelliJ IDEA*, FTfJP 2021
pdf
2020
Oebele Lijzenga and Tom van Dijk, *Symbolic Parity Game Solvers that Yield Winning Strategies*, GandALF 2020
pdf
2019
Tom van Dijk, *A Parity Game Tale of Two Counters*, GandALF 2019
pdf talk
2019
Tom van Dijk, Jeroen Meijer and Jaco van de Pol, *Multi-core On-The-Fly Saturation*, TACAS 2019
doi pdf talk
2019
Tom van Dijk and Bob Rubbens, *Simple Fixpoint Iteration To Solve Parity Games*, GandALF 2019
pdf talk
2018
Tom van Dijk, *Attracting Tangles to Solve Parity Games*, CAV 2018
doi pdf talk
2018
Tom van Dijk and Jaco van de Pol, *Multi-core Decision Diagrams*, Handbook of Parallel Constraint Reasoning
doi pdf
2018
Tom van Dijk and Jaco van de Pol, *Multi-core symbolic bisimulation minimisation*, STTT
doi pdf
2018
Tom van Dijk, *Oink: An Implementation and Evaluation of Modern Parity Game Solvers*, TACAS 2018
doi pdf talk
2018
Tom van Dijk, Rüdiger Ehlers and Armin Biere, *Revisiting Decision Diagrams for SAT*, arXiv
arxiv pdf
2017
Wytse Oortwijn, Tom van Dijk and Jaco van de Pol, *Distributed binary decision diagrams for symbolic reachability*, SPIN 2017 (Best paper)
doi pdf
2017
Armin Biere, Tom van Dijk and Keijo Heljanko, *Hardware model checking competition 2017*, FMCAD 2017
doi pdf
2017
Tom van Dijk and Jaco van de Pol, *Sylvan: multi-core framework for decision diagrams*, STTT
doi pdf
2017
Tom van Dijk, Robert Wille and Robert Meolic, *Tagged BDDs: Combining reduction rules from different decision diagram types*, FMCAD 2017
doi pdf talk
2016
Tom van Dijk and Jaco van de Pol, *Multi-core symbolic bisimulation minimisation*, TACAS 2016
doi pdf talk
2016
Tom van Dijk, *Sylvan: Multi-core Decision Diagrams*, PhD Thesis
doi pdf
2015
Tom van Dijk, Ernst Moritz Hahn, David N. Jansen, Yong Li, Thomas Neele, Mariëlle Stoelinga, Andrea Turrini and Lijun Zhang, *A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking*, SETTA 2015
doi pdf
2015
Wytse Oortwijn, Tom van Dijk and Jaco van de Pol, *A Distributed Hash Table for Shared Memory*, PPAM 2015
doi pdf
2015
Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom and Tom van Dijk, *LTSmin: High-Performance Language-Independent Model Checking*, TACAS 2015
doi pdf
2015
Tom van Dijk and Jaco van de Pol, *Sylvan: Multi-Core Decision Diagrams*, TACAS 2015
doi pdf talk
2014
Tom van Dijk and Jaco van de Pol, *Lace: Non-blocking Split Deque for Work-Stealing*, MuCoCOS 2014
doi pdf talk
2012
Tom van Dijk, Alfons Laarman and Jaco van de Pol, *Multi-core and/or Symbolic Model Checking*, AVoCS 2012
doi pdf
2012
Tom van Dijk, Alfons Laarman and Jaco van de Pol, *Multi-Core BDD Operations for Symbolic Reachability*, PDMC 2012
doi pdf

**PhD Thesis**(2016)

*Sylvan: Multi-core Decision Diagrams*, University of Twente.**MSc Thesis**(2012) [cum laude]

*The parallelization of binary decision diagram operations for model checking*, University of Twente.

Awarded an honorary mention (2nd place) of the Dutch national M&I Informatie Scriptieprijs 2012.**BSc Thesis**(2010)

*Analysing And Improving Hash Table Performance*, University of Twente.

**Program committees**: FMCAD 2018 Student Forum, TACAS 2019 Artifact Evaluation, ATVA 2019 Artifact Evaluation, AVoCS 2019, FTSCS 2019, AVERTIS 2019, TACAS 2020, SAC-SVT 2020, SPIN 2021, SAC-SVT 2021, SAC-SVT 2022, FMCAD 2022 Student Forum, SAC-SVT 2023, FORTE 2023 Artifact Evaluation (chair).**Organisation**: Dutch Model Checking Day 2016, Hardware Model Checking Competition 2017, FMCAD 2018, 2019 Webmaster, SETTA 2019 Publicity Chair (Europe)**External Reviewer**: SPIN 2014, ICFEM 2014, FASE 2016, ATVA 2016, TACAS 2017, FCT 2017, TACAS 2018, SAT 2018, FORTE 2018, CSL 2018, FMCAD 2018, FoSSaCS 2019, LICS 2019, VMCAI 2020, LICS 2020, FoSSaCS 2021, TACAS 2021, CONCUR 2021, TACAS 2022, FoSSaCS 2022, FORTE 2022, NFM 2022, FoSSaCS 2023, CONCUR 2023.**Journal Reviewer**: IEEE Transactions on Computers (2014), Formal Methods in System Design (2018), Software Tools for Technology Transfer (2018, 2019), MDPI Algorithms (2018), VLSI Integration (2018), JSAT (2019), JAR (2019).

Formal Methods and Tools

Zilverling 3035
University of Twente

E-mail: t dot vandijk at utwente dot nl.