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