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 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. I 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 controller 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.
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.
Design projects are for students who work in a group to design a piece of software, i.e., Module 11 TCS students.
Topics on parity games:
Related to parallel programming, that is, load balancing by work stealing (my Lace framework):
Other 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):
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.
Formal Methods and Tools
Zilverling 3035
University of Twente
E-mail: t dot vandijk at utwente dot nl.