My main research interests are in testing, model checking, semantics, algorithmic game theory, parameterised Boolean equation systems (PBESs), semantics, automata and language theory, and more broadly, any method or technique that helps in improving the state of affairs in software engineering.

Have a look at our verification tool suite mCRL2 to which I contribute in some way or another.


  • 2016, project leader in the industry-funded follow-up on VICTORIA.
  • 2014-2015, project leader in the FP7 TTP VICTORIA, a project exploring the connexion between the industrial language Dezyne and mCRL2.
  • 2010-2013, project leader in the NWO-project VOCHS, a project on verifying the control software of the CMS experiment at the Large Hadron Collider (CERN), using the framework of parameterised Boolean equation systems.
  • 2006-2009, project leader in the NWO-project COMFORTS, a project on verification of data-dependent and real-time systems using parameterised Boolean equation systems.
  • 2005-2006, project leader of Line of Attention 3 in the Senter-project TANGRAM, a project on model-based testing and integration in industry.