Tom van Dijk

My Research 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.
• See also my Github repositories

Teaching

• 2019 Software science: Parity Games (2.5 EC course in the Computer Science Master)
  • Lecture 1: LTL, CTL and mu-Calculus
  • Lecture 2: Attractor-based algorithms
  • Lecture 3: Progress measures algorithms
  • Lecture 4: Strategy iteration and fixed point iteration
  • Tutorial/Homework: Students implement algorithms in Python
  • Slides of all lectures
• 2019–2020 Software Systems (Module 2 of the Computer Science Bachelor, 15 EC)
  • I am one of the teachers of the Programming line
• 2020 Software science: Model Checking and Parity Games (5 EC course in the Computer Science Master)
  • This will be a redesign of last year’s course, also incorporating material from earlier courses

Projects

Students (BSc, MSc, etc) are welcome to study questions about parity games with me. I have a number of open questions and assignments available.

Design projects

Design projects are for students who work in a group to design a piece of software.

• A graphical user interface to understand and develop parity game algorithms. The idea is to have a GUI where a user can create, load, change a parity game which can be solved using various algorithms. The step-by-step execution of the algorithm can be followed by the tool, so the algorithm can be halted at each step. The primary goal of this tool is to help parity game researchers understand their algorithms. Secondary goals include using the tool as a teaching aid in the model checking course, and to have a reasonably easy to extend framework for studying various other graph-based algorithms. Some work on a related topic has been done by Daan Kooij as part of his BSc project to visualize “priority promotion” using the graph transformation tool Groove. The design project has different aims than Daan’s research project.

BSc/MSc Research topics

• Can you efficiently derive a strategy for the winning player in the fixpoint algorithm?
  Now solved, see this paper with Bob Rubbens.
• What is a (parameterised) lower bound game for the quasi-polynomial parity game solving algorithms?
• Can you implement Lehtingen’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 to do incremental parity game solving quickly?
  LTL synthesis solvers like STRIX generate a parity game, but while generating, already try to solve the partial generated games. To investigate is whether we can impr
• Can we find (prove that there must be) ordered trees in every parity game solver?
  This topic might actually be best suited for an ambitious MSc student.

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

• Can you prove the correctness of algorithms like “priority promotion” and “tangle learning”?
  This is a suitable topic for BSc and MSc students, as the amount of work is easy to scale for either BSc or MSc level. The end-goal of this project is to prove correctness of a large number of algorithms and we are currently studying the recursive algorithm and the priority promotion algorithm. However, there are many other algorithms that we would like to prove properties about.
• Can you prove that the “Two Counters” parameterised parity game is exponential for several parity game algorithms?

On using binary decision diagrams to solve parity games symbolically:

• Can you implement the new fixpoint algorithms (with freezing / justifications) using binary decision diagrams?
  This topic is suitable for an ambitious BSc student.
• Can you implement the “tangle learning” algorithm using binary decision diagrams?
  This topic is suitable for an ambitious MSc student. The challenge is to find a good way to encode tangles using binary decision diagrams.

Related to parity games are questions like:

• Can we foresee tangles in the translation of LTL synthesis/model-checking to Parity Games?
  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.
• Can we use tangle learning effectively instead of strategy iteration for fast LTL synthesis?
  The STRIX tool that solves LTL synthesis via parity games uses strategy iteration. The idea is to substitute this by using Oink (my parity game solver) and plug in different algorithms. This topic is suitable for BSc and MSc students.
• How to use tangles 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. This topic is suitable for MSc students.

There are also open questions on other topics in my research:

• How do the load balancing frameworks Lace, Cilk, OpenMP and Intel TBB compare?
  This topic is suitable for BSc students.
• Can you prove with a theory prover that the work stealing deque in Lace is correct?
  This topic is suitable for BSc students.
• How to implement and tune parallel dynamic variable reordering for BDDs in Sylvan?
  If you can tune this well enough, you could participate in the SYNTCOMP competition.
  I currently have a prototype implementation of dynamic variable reordering, but I have no time to finish it. If you like, you could build a MSc topic out of it.
• How can we do fast incremental MaxSAT queries for a reasonably sized product-feature database?

Publications

Theses

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

Academic Service

• Program committees: FMCAD 2018 Student Forum, TACAS 2019 Artifact Evaluation, ATVA 2019 Artifact Evaluation, AVoCS 2019, FTSCS 2019, TACAS 2020, SAC-SVT 2020
• 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.
• 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).

Contact

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