Contact me or drop by for MSc projects on model checking and model-based testing, or their (industrial) application.
- Former PhD students:
- Olav Bunte, PhD. 2018-2024 (thesis). Currently University Teacher at TU/e.
- Mark Bouwman, PhD. 2018-2023 (thesis). Last known affiliation: Rijkswaterstaat.
- Maurice Laveaux, PhD. 2018-2022 (thesis). Currently Scientific Programmer at TU/e.
- Thomas Neele, PhD. 2016-2020 (thesis). Currently Assistant Professor at TU/e.
- Ulyana Tikhonova, PhD. 2011-2017 (thesis). Last known affiliation: F1re.
- Daniela Remenska, PhD. 2011-2016 (at NIKHEF and VU Amsterdam). Last known affiliation: eBay.
- Maciej Gazda, PhD. 2010-2016 (thesis). Now at University of Sheffield.
- Neda Noroozi, PhD. 2010-2014 (thesis). Last known affiliation: ALTRAN.
- Jeroen Keiren, PhD. 2009-2013 (thesis). Currently Assistant Professor at the TU/e.
- Bas Ploeger, PhD. 2005–2009 (thesis). Last known affiliation: Google Zurich.
- Former MSc students:
- Diederik Geertzen. Modelling and Verification of Parallelized List Decision Diagram Algorithms. January 2024 — December 2024.
- Jordi van Laarhoven. Formalising the State Machine Modelling Tool (SMMT). March 2023 — December 2023.
- Edward Liem. Extraction of Invariants in Parameterised Boolean Equation Systems. March 2023 — September 2023. Graduated Cum Laude.
- Myrthe Spronck. Fairness Assumptions in the Modal mu-Calculus. March 2023 — September 2023. Graduated Cum Laude.
- Tom Buskens. Optimizing the code generator for OIL. February 2021 — October 2021.
- Koen Degeling. New algorithms and heuristics for solving Variability Parity Games. February 2021 — November 2021.
- Anneke Huijsmans. Optimising Parity Game Solvers using dynamic SCC maintenance. November 2020 — September 2021.
- Geert van Ieperen. Visualisation of large Labelled Transition Systems. April 2020 — February 2021.
- Sjef van Loo. Verifying SPLs using parity games expressing variability. May 2019 — November 2019.
- Mark Frenken. Code Generation and Model-Based Testing in Context of OIL. April 2019 — December 2019.
- Kevin Nogarede. An approachable language for formal requirements. April 2019 — December 2019.
- Maurice Laveaux. Abstracting Real-Valued Parameters in Parameterised Boolean Equation Systems. April 2017 — January 2018. Graduated Cum Laude.
- Roxana Paval. Modeling and Verifying Concurrent Data Structures. Joint supervision with Bas Luttik. March 2017 — January 2018.
- Olav Bunte. Quantitative Model Checking on Probabilistic Systems using pLµ. February 2017 — November 2017. Graduated Cum Laude.
- Myrthe van Delft. Consistent Consequence Formalized. January 2016 — July 2016. Joint supervision with Herman Geuvers.
- Petra van den Helder. Verification of PLC code used at CERN. March 2015 — May 2016. Joint supervision with Dragan Bosnacki.
- Tessa Belder. State space reduction for state-based and event-based models of Software Product Lines, December 2014 — July 2015. Joint supervision with Erik de Vink. Graduated Cum Laude.
- Pieter Bootsma. Speeding up the small progress measures algorithm for parity games using the GPU, March 2013 — December 2013. Joint supervision with Andrei Jalba and Herman Haverkort. Graduated Cum Laude.
- Mark Geelen. Black-box Random Testing of the mCRL2 Toolset Using Attribute Grammars. March 2013 — January 2014. Joint supervision with Wieger Wesselink.
- Kevin van der Pol. Symbolic compositional model checking for mCRL2, March 2012 — January 2013. Graduated Cum Laude.
- Tom Boshoven. A Symbolic Approach to PBES instantiation, March 2012 — February 2013.
- Sander Leemans. Validation of CERN\’s Finite State Machines, September 2011 — June 2012. Research carried out at CERN. Joint supervision with Jeroen Keiren. Graduated Cum Laude.
- Charl Linssen. Diagnostics for Model Checking, March 2010 — January 2011.
- Jeroen Keiren. An experimental study of algorithms and optimisations for parity games, with an application to Boolean Equation Systems, February 2009 — July 2009. Graduated Cum Laude.
- Tom Haenen. Strengthening methods for parameterized Boolean equation systems, March 2009 — September 2010.
- Simon Janssen. Tools for Parameterized Boolean Equation Systems, February 2008 — August 2008.
- Henk van de Crommert. Robotic devices as interfaces to Web services, March 2007 — October 2007.
- Alexander van Dam. Instantiation of Parameterised Boolean Equation Systems, September 2006– August 2007.
- Former EngD students:
- George Azis (2021)
- Trupti Manik (2019)
- Sololia Ayele (2018)
- Aldo Daniel Martinez Marquez (2016)
- Erikos Alkalai (2015)
- Tesfahun Tesfay (2015)
- Christos Apostolou (2014)
- Abelneh Teka (2014) won the design award.
- Sanda Contiu (2008)
- Dmitri Jarnikov(2003)
- MSc. Seminars/Internships/Capita Selecta
- Martijn Struijs, Consistent Consequence for PBESs, April 2018 — June 2018; joint supervision with Herman Geuvers.
- Lisette Sanchez, BDD-based Parity Game Solving, November 2017 — January 2018. An extended and enhanced version is available here
- Mark Bouwman, Liveness Analysis in Process Algebra, November 2017 — January 2018.
- Maurice Laveaux, Implementing Priority Promotion for Parity Games, November 2016 — January 2017.
- Myrthe van Delft, A proof system for Consistent Consequence on PBES, May–August 2015; joint supervision with Herman Geuvers.
- Ka ka Tam, Robustness in Asynchronous Model-Based Testing, May–August 2015.
- Bram Geron, Verifying Compiler Rules, internship INRIA-Lille, September–November 2012.
- Kevin van der Pol, Compositional Verification Techniques for mCRL2, September 2011 — January 2012.
- Tom Boshoven, Simulation Equivalence Reduction in Parity Games, September 2011 — January 2012.
- Kevin van der Pol, Applying Gauss Elimination from Boolean Equation Systems to Simple Integer Equation Systems, September 2011 — January 2012. Join supervision with Jeroen Keiren.
- Vincent Kusters, Preprocessing parity games with partial Gauss elimination, September 2010–January 2011.
- Rob Schoren, Correspondence between Kripke Structures and Labeled Transition Systems for Model Minimization, September 2010–January 2011.
- Shreya Adyanthaya. Adding Symmetry Reduction Techniques to mCRL2, September 2010–January 2011. Joint supervision with Mohammad Mousavi.
- Vincent Kusters. An Analysis of the CMS Control Software, internship CERN, March 2010–June 2010.
- Maarten Meulen. Combining Bounded Model Checking with Highway Search, September 2008– December 2008.
- Jeroen Keiren. Small Progress Measures, Parity Games and Boolean Equation Systems, September 2008– December 2008.
- Simon Janssen. Conjunctive and Disjunctive Boolean Equation Systems, September 2007– December 2007.