Academic software


mCRL2 is a complete toolset for model checking processes. I have worked on several approaches to perform model checking on real-time systems. The tools I have worked on are lpsrealzone, lpssymbolicbisim and pbessymbolicbisim. The latter two are actually more general and can also deal with other kinds of infinite-state systems.


For my master thesis, I have improved the GPU model checking tool GPUexplore. I added partial-order reduction to improve the memory efficiency and improved the speed with a factor 11 over the previous version. This brought the total speed-up over a single-threaded implementation to well over a hundred times. The thesis has been awarded with the Ngi-NGN Informatie Scriptieprijs (second prize) in 2016 and was nominated for the ENIAC best thesis award.


During an internship at Institute of Software, Chinese Academy of Sciences, I added symbolic bisimulation minimization of probabilistic systems to IscasMC. In addition, I added the parallel BDD package Sylvan as symbolic back-end.

Non-academic projects


A HTML5 remake of the game "Achtung die Kurve", created together with Joost van Doorn and Nick Schot. This game is basically a multiplayer version of snake where you never stop growing. The goal is to outmaneuver your friends. Using multiple keyboards is recommended. Most of this was put together in one weekend. A playable version can be found here and the source can be found on Github.

This website

This website is implemented in Haskell, a purely functional language, and uses the Yesod web framework. Haskell's type system helps prevent security problems and prevents almost all the runtime bugs. The sources are on Github.

Android apps

I have worked on several Android apps within student associations at the University of Twente. I have also published my own application.