Below we show examples of topics for master and bachelor (research) projects; click on the title to see a more detailed description. Even when you don’t find what you want you can contact one of our staff members. Typically they have additional interesting projects not explicitly listed.
Master’s projects
- An ACO approach to parity games (supervisor: De Vink)
- Paradigm protocol verification (supervisor: De Vink)
- Probabilistic bisimulation (supervisor: De Vink)
- Extracting and exploiting invariants for solving PBESs (supervisor: Willemse)
- Formal modelling and verification of protocols for cyber physical systems kernel (supervisor: Willemse)
- Optimising Parity Game Solvers using dynamic SCC maintenance (supervisor: Willemse)
- Algorithms for Variability Parity Games (supervisor: Willemse; international collaboration)
- Automata learning (supervisor: Zantema)
- Various industrial and/or theoretical explorations (supervisor: Groote)
- mCRL2 with shared variables (supervisor: Luttik/Willemse)
- Process algebra with signals (supervisor: Luttik)
-
Refining our confidence in refinable partition data structures (supervisor: Keiren)
Bachelor’s projects
- Modelling and verifying a non-atomic dual bakery algorithm with bounded tokens in mCRL2 (supervisor: Luttik)
- Implementing a fast graph positioning algorithm (supervisor: Groote)
- Design and possibly implement a fast parallel aterm library (supervisor: Groote)
- Translate CIF to mCRL2 (supervisor: Groote)
Recently finished projects
- MSc Defence 27 November 13.00 - 13.45, 2020, MS Teams.
Wouter Schols: Verification of an iterative implementation of Tarjan’s algorithm for Strongly Connected Components using Dafny. - MSc Defence 21 October 10.00 - 10.30, 2020, MS Teams.
Bram Hooimeijer: Model Inference for Legacy Software in Component-Based Architectures. - MSc Defence 21 September 13.30 - 14.00, 2020, MS Teams.
Nikita Golovliov: Verification of Multiprocessor System Memory Model. - MSc Defence 21 September 10.00 - 10.30, 2020, Atlas 2.215.
Wessel Sinnema: Verifying memory consistency in mCRL2. - MSc Defence 18 August 15.30 - 16.00, 2020, Atlas 2.320.
Sebastiaan Verhoek: SMT solver verification of ladder logic in a production environment (Tata Steel).
Examples of all projects since 2017 can be found here.