I am a postdoctoral researcher at the Institute for Formal Models and Verification at the Johannes Kepler University Linz. I am doing research into parallelizing SAT-solving and efficient solving of parity games. I like making and improving tools for research, in particular model checking, and searching for better algorithms for open problems. I obtained my PhD (thesis) in the Formal Methods and Tools group at the University of Twente, where I performed research on parallelizing decision diagram algorithms.
Institute for Formal Models and Verification
Johannes Kepler University Linz
E-mail: tom dot vandijk at jku dot at.
- High-Performance Research Tools
- Parity Games
- Symbolic methods for model checking (SAT, BDD, IC3)
- Parallel Algorithms and Data Structures
-  Tom van Dijk, A Parity Game Tale of Two Counters [arXiv]
-  Tom van Dijk, Rüdiger Ehlers, and Armin Biere, Revisiting Decision Diagrams for SAT.
-  Tom van Dijk, Attracting Tangles to Solve Parity Games, CAV 2018, Accepted, [arXiv, talk, DOI].
-  Tom van Dijk, Oink: an Implementation and Evaluation of Modern Parity Game Solvers, TACAS 2018, Accepted, [arXiv, DOI].
-  Tom van Dijk, Robert Wille and Robert Meolic, Tagged BDDs: Combining reduction rules from different decision diagram types, FMCAD 2017, [DOI].
-  Armin Biere, Tom van Dijk, Keijo Heljanko, Hardware model checking competition 2017, FMCAD 2017, [DOI].
-  Wytse Oortwijn, Tom van Dijk and Jaco van de Pol. Distributed Binary Decision Diagrams for Symbolic Reachability, SPIN 2017, Best paper award, [DOI].
-  Tom van Dijk and Jaco van de Pol, Multi-Core Symbolic Bisimulation Minimisation, STTT special issue invited paper, Submitted.
-  Tom van Dijk and Jaco van de Pol, Sylvan: Multi-core Framework for Decision Diagrams, STTT special issue invited paper (October 2016) [DOI]
-  Tom van Dijk and Jaco van de Pol, Multi-Core Symbolic Bisimulation Minimisation, TACAS 2016, Eindhoven, Netherlands (April 2016) [DOI]
-  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, Nanjing, China (November 2015) [DOI]
-  Wytse Oortwijn, Tom van Dijk and Jaco van de Pol, A Distributed Hash Table for Shared Memory, Parallel Processing and Applied Mathematics (September 2015)
-  Tom van Dijk and Jaco van de Pol, Sylvan: Multi-core Decision Diagrams, TACAS 2015, London, UK (April 2015) [DOI]
-  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, London, UK (April 2015) [DOI]
-  Tom van Dijk and Jaco van de Pol, Lace: Non-blocking Split Deque for Work-Stealing, 7th Intl Workshop on Multi/many-Core Computing Systems, Porto, Portugal (August 2014) [DOI]
-  Tom van Dijk, Alfons Laarman and Jaco van de Pol, Multi-core and/or Symbolic Model Checking, invited paper to AVOCS 2012, Bamberg, Germany (September 2012) [DOI]
-  Tom van Dijk, Alfons Laarman and Jaco van de Pol, Multi-Core BDD Operations for Symbolic Reachability, 11th Intl Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012, London, UK (September 2012) [DOI]
-  Sylvan: Multi-core Decision Diagrams, PhD Thesis, University of Twente, July 2016
-  The parallelization of binary decision diagram operations for model checking, M.Sc. Thesis (cum laude), University of Twente, April 2012
Awarded an honorary mention (2nd place) of the Dutch national M&I Informatie Scriptieprijs 2012.
-  Analysing And Improving Hash Table Performance, B.Sc. Thesis, University of Twente, 2010
- 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.
- A collection of game modification tools (around 2000-2003) written in Visual C++ to customize the computer game The Sims. One of these programs was published and sold worldwide by Abacus under the name Career Creator Pro.
- Two consecutive projects involving high-speed real-time sensor controller software in C for a R&D project of Scangineers/Scanpoint, a company that developed Self Service Checkouts. I was the (only) software developer (freelance) for these two projects.
- Secretary of the board (2006-2007) of the student association VGST.
- Chairman (2012-2013) of the Jonge Democraten Twente, the regional department of the Jonge Democraten, a political youth organisation associated with the national party D66.
- As part of a team of volunteer developers, I’ve worked on several web development projects for the Jonge Democraten, see my GitHub.
- As a member of both the Economy and the Sustainability study groups of the Jonge Democraten, I helped organize a national symposium (“Duurzaam denken & duurzaam ondernemen”, January 2015) on environmental sustainability in business, in which I managed technical aspects and organized several speakers.