Tom van Dijk

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, the application of parity games in reactive (LTL) synthesis, using binary decision diagrams in formal methods, and 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.

Since my return at the University of Twente, I have continued my research into parity games. I have 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 machine 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.

My Research Tools

Teaching

Research projects for students

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.

BSc Design projects

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

BSc Research topics

Topics on parity games:

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

Other topics:

MSc Research topics

Topics on parity games:

Related to parity games are questions like:

On using binary decision diagrams to solve parity games symbolically:

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

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

Capita Selecta topics

Collaboration

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.

Publications and Talks

2024 Tom van Dijk, Feije van Abbema and Naum Tomov, Knor: reactive synthesis using Oink, TACAS 2024 doi pdf 2024 Tom van Dijk, Reproducing parity game algorithms in Oink, RRRR 2024 pdf 2024 Tom van Dijk, Georg Loho and Matthew T. Maat, The Worst-Case Complexity of Symmetric Strategy Improvement, CSL 2024 doi pdf 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 doi pdf 2020 Oebele Lijzenga and Tom van Dijk, Symbolic Parity Game Solvers that Yield Winning Strategies, GandALF 2020 doi 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

Theses

Academic Service

Contact

Formal Methods and Tools
Zilverling 3035 University of Twente
E-mail: t dot vandijk at utwente dot nl.