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.


  • 2018-2023, principal investigator in the industry-funded project VOICE-B (2018-2023), a project on adding verification technology to Model-Driven Engineering solutions developed at Océ (funded by Océ-Technologies B.V.)
  • 2018-2022, co-applicant in the NWO-TOP project AVVA, a project on exploring the use of massive parallelism to speed up verification and the use of verification to assess the correctness of parallel programs.
  • 2016, project leader in an industry-funded (by Verum B.V.) follow-up on VICTORIA.
  • 2014-2015, principal investigator in the FP7 TTP VICTORIA, a project exploring the connexion between the industrial language Dezyne and mCRL2.
  • 2010-2013, principal investigator 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, principal investigator 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.