I'm an associate professor in, and the head of the Formal System Analysis group of the CS department at the TU/e, and a senior research fellow at TNO/ESI.

My research is in Algorithms and Logics for VErification (ALIVE), and, more broadly, in all means and methods that help designing correct and reliable systems. I work on algorithms and theory for PBES, fixed point logics, parity games and model-based testing theories, and applications of model checking. My PBES theory drives the verification technology offered by the tool suite mCRL2 to which I contribute in some way or another.

Have a look at our past work verifying the control software of experiments at the LHC at CERN, developing tools and helping improve the quality of the software.

Drop me a mail if you think I (or my group) can help you with improving your (software) designs.

For MSc students looking for MSc final projects: there are external opportunities (e.g. Canon, ASML, Verum) and within our group (see, e.g., this assignment or this assignment; feel free to drop by to discuss other possibilities).


RESEARCH GRANTS (PI/co-applicant)
  • Verification of OIL Interfaces and Components for Engineers-B (VOICE-B, funded by Océ-Technologies B.V. (Canon production printing, these days); PI), 2018--2023.
  • Accelerated Verification and Verified Acceleration (AVVA, NWO TOP grant; co-applicant), 2018--2023.
  • Verification In the Cloud TO Radically Improve Analyses (VICTORIA, FP7 grant; PI), 2014--2015.
  • Verification of Complex Hierarchieval Systems (VOCHS, NWO grant; PI), 2010--2016.
  • A Common Framework for Reactive and Timed Systems (COMFORTS, NWO grant; PI), 2006--2009.


Prior to my current position, I held the following posts:
  • from September 2009 to September 2019, I had a part-time affiliation as a software engineer at CERN.
  • until December 2017, I was the managing director of the national research school IPA.
  • until June 2016, I worked as an assistant professor in the MDSE section.
  • from September 2006 to September 2009, I worked as an assistant professor in the context of the NWO-funded BRICKS/FOCUS project COMFORTS on verification of reactive and timed systems using parameterised Boolean equation systems.
  • from February 2004 to September 2006, I worked as an industrial post-doctoral researcher at ASML in the Dutch Senter project Tangram on model-based methods for testing, diagnosis and integration. From January 2006 to September 2006, I was project leader of Line of Attention 3, responsible for Model-Based Testing methodology.
  • from November 2002 to January 2004, I worked as a researcher in Action 1 of the European project Artist. Also have a look at this book that was one of the results of this yearlong collaboration.
  • from October 1998 to November 2002, I was a PhD student at the TU/e, working under contract 612-014-008 of the Dutch Organisation for Scientific Research (NWO).
  • from October 1997 to July 1998, I did my Master's project at the company CMG (now called Logica) in the division ATG, The Hague.