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

Past Master Projects

• Danny van Dortmont: Easy Property Specification Through UML State-Machine Diagrams.
  
• Kas Burgers: Family-based Fault-tree Analysis.
  
• Diederik Geertzen: Modelling and Verification of Parallelized List Decision Diagram Algorithms.
  
• Willem Rietdijk: Compositional verification of control software UML models.
  
• Stijn Kuiper: Complete Axiomatisations of Interleaving with Deadlock and Successful Termination.
  
• Erik Pardijs: Finite bases in the linear time-branching time spectrum with sequential composition and succesful termination.
  
• Jordi van Laarhoven: Formalising the State Machine Modelling Tool (SMMT).
  
• Jore Booy: Model-Based Mocking: Compositional Model-Based Testing for Microservices using the Axini Modeling Platform.
  
• Isabelle Cooijmans: Verification of EULYNX light signal using mCRL2 and comparing with auto-translated model.
  
• Edward Liem: Extraction of Invariants in Parameterised Boolean Equation Systems.
  
• Myrthe Spronck: Fairness Assumptions in the Modal mu-Calculus.
  
• Gijs Leemrijse: Towards relaxed memory semantics for the Autonomous Data Language.
  
• Tim Beurskens: Formal Verification of Safety Properties in Automotive Systems.
  
• Sky Sarah van Grieken: Replicating Experiments and Improving Algorithms for Exact DFA Identification.
  
• Maarten Visscher: Formal verification on the Maeslant Barrier Locomobile software.
  
• 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