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 am currently designing algorithms that solve parity games. Hopefully one of these runs in polynomial time.
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.
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
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 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?
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).
Formal Methods and Tools
University of Twente
E-mail: t dot vandijk at utwente dot nl.