Tom van Dijk

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.

Contact

Institute for Formal Models and Verification
Johannes Kepler University Linz
E-mail: tom dot vandijk at jku dot at.

Github

https://www.github.com/trolando/

Research interests

  • High-Performance Research Tools
  • Parity Games
  • Symbolic methods for model checking (SAT, BDD, IC3)
  • Parallel Algorithms and Data Structures

Publications

  • [2018] Tom van Dijk, Rüdiger Ehlers, and Armin Biere, Revisiting Decision Diagrams for SAT.
  • [2018] Tom van Dijk, Attracting Tangles to Solve Parity Games, CAV 2018, Accepted, [arXiv].
  • [2018] Tom van Dijk, Oink: an Implementation and Evaluation of Modern Parity Game Solvers, TACAS 2018, Accepted, [arXiv].
  • [2017] Tom van Dijk, Robert Wille and Robert Meolic, Tagged BDDs: Combining reduction rules from different decision diagram types, FMCAD 2017, [DOI].
  • [2017] Armin Biere, Tom van Dijk, Keijo Heljanko, Hardware model checking competition 2017, FMCAD 2017, [DOI].
  • [2017] Wytse Oortwijn, Tom van Dijk and Jaco van de Pol. Distributed Binary Decision Diagrams for Symbolic Reachability, SPIN 2017, Best paper award, [DOI].
  • [2016] Tom van Dijk and Jaco van de Pol, Multi-Core Symbolic Bisimulation Minimisation, STTT special issue invited paper, Submitted.
  • [2016] Tom van Dijk and Jaco van de Pol, Sylvan: Multi-core Framework for Decision Diagrams, STTT special issue invited paper (October 2016) [DOI]
  • [2016] Tom van Dijk and Jaco van de Pol, Multi-Core Symbolic Bisimulation Minimisation, TACAS 2016, Eindhoven, Netherlands (April 2016) [DOI]
  • [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, Nanjing, China (November 2015) [DOI]
  • [2015] Wytse Oortwijn, Tom van Dijk and Jaco van de Pol, A Distributed Hash Table for Shared Memory, Parallel Processing and Applied Mathematics (September 2015)
  • [2015] Tom van Dijk and Jaco van de Pol, Sylvan: Multi-core Decision Diagrams, TACAS 2015, London, UK (April 2015) [DOI]
  • [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, London, UK (April 2015) [DOI]
  • [2014] 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]
  • [2012] 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]
  • [2012] 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]

Theses

Tools

  • 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.

Other accomplishments

  • 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.