Below, we provide an overview of finished bachelor and master projects. Examples of currently available projects can be found here.

Past Master Projects

• Milan Hutten: Sound and Complete Axiomatizations for the rooted variants of Divergence-Preserving, Weak Divergence-Preserving and Stability-Respecting Branching Bisimilarity.
  
• Kevin Jilissen: A formal analysis of the tunnel control systems of the Rijkswaterstaat GITO.
  
• Floris Zeven: Spatial Model Checking with mCRL2.
  
• Dennis Rizvić: Making MCA easily understandable with mCRL2.
  
• Koen Degeling: New algorithms and heuristics for solving Variability Parity Games.
  
• Tom Buskens: Optimizing the code generator for OIL.
  
• Anneke Huijsmans: Optimising parity game solvers using dynamic SCC maintenance.
  
• Jasper Stam: Formal verification of an industrial PLC program in Function Block Diagram and Structured Text.
  
• Geert van Ieperen: Visualisation of large Labelled Transition Systems.
  
• Wouter Schols: Verification of an iterative implementation of Tarjan’s algorithm for Strongly Connected Components using Dafny.
  
• Bram Hooimeijer: Model Inference for Legacy Software in Component-Based Architectures.
  
• Nikita Golovliov: Verification of Multiprocessor System Memory Model.
  
• Wessel Sinnema: Verifying memory consistency in mCRL2.
  
• Sebastiaan Verhoek: SMT solver verification of ladder logic in a production environment (Tata Steel).
  
• Elbert van de Put: Ant Colony Optimization for Model Checking.
  
• Mark Frenken: Code Generation and Model-Based Testing in Context of OIL.
  
• Sjef van Loo: Verifying SPLs using parity games expressing variability.
  
• Stan Roelofs: Automatically proving equality of infinite sequences.
  
• Msc presentation Johri van Eerd.
  
• Kevin Nogarede: An approachable language for formal requirements.
  
• Ruud Meeuws: Model Checking Supermodels Workbench with mCRL2.
  
• Mark Bouwman: A model-based test platform for rail signalling systems.
  
• Hong Zhang: Quality metrics for ASOME data models.
  
• Ferry Timmers: A complete axiomatisation for probabilistic trace equivalence.
  
• Lisette Sanchez: Learning software behavior through active automata learning with data.
  
• Lois Nijland: Adding sequential composition and termination to the linear time – branching time spectrum.
  
• Astrid Belder: Decidability of bisimilarity and axiomatisation for sequential processes in the presence of intermediate termination.
  
• Marijn Rol: Verification of ASD multi-component systems in mCRL2.
  
• Ziad Ben Snaiba: Logics and Algorithms for Product and Family-Based Analysis of Software Product Lines.
  
• Ruud van Vijfeijken: Performance evaluation of network on chip using formal models.
  
• Maurice Laveaux: Abstracting real-valued parameters in parameterised Boolean equation systems.
  
• Roxana Paval: Modeling and Verifying Concurrent Data Structures.
  
• Perry van Wesel: Formal analysis of ring networks.
  
• Olav Bunte: Quantitative model checking on probabilistic systems using plmu*+.
  

Past Bachelor Projects