MSc Projects

This webpage holds a list of available, in progress and completed Master projects at FMT. If you are interested in carrying out a MSc assignment at the FMT group, please contact dr. Tom van Dijk and dr. Arnd Hartmanns, the study advisors of FMT.

If you want to do your MSc Final Project with FMT, you will first prepare the research in the course Research Topics (10 EC). You will need to find a subject (or subject area) and a supervisor. You can have one or more supervisors for the Research Topics course, but at least one must be connected to the UT. You must then register for Research Topics in Canvas and via the Mobility Online application. During your Research Topics, you study the background of the subject and prepare research questions and a detailed planning. Afterwards, you receive a grade for Research Topics and can start your Final Project (30 EC). You must register again for Final Project in Canvas and via the Mobility Online application. For the Final Project, you will need two supervisors and at least one of them must be a member of the FMT group.

Available

Algorithms and Data Structures

Correct and efficient algorithms and datastructures for concurrency and model checking.

Deductive Verification for LLVM-IR ()
Parity game algorithms (T. van Dijk)
Consider It Parsed (dr. V Zaytsev)
Does your model make sense? (Prof.dr. M.I.A. Stoelinga)
Formal Verification of Efficient Data Structures for Web Services to Automotive Lease Companies (dr. S.C.C. Blom, prof.dr. M. Huisman)
Safety verification of Deep Neural Networks for highly automated driving (Dr.-Ing. E.M. Hahn, V.H. Hashemi)
Projects related to Probabilistic Model Checking: Theory, Algorithms, Implementation, Modelling (Dr. A. Hartmanns)
Risk Assessment of Water Supply Networks (MSc L Jimenez Roa, Prof.dr. M.I.A. Stoelinga)
JANI for the web (Dr.-Ing. E.M. Hahn)

Case studies and Applications

Application of formal methods to practical examples.

Using model-based techniques for integration of subsystems (dr.ir. G.J. Tretmans)
Translating RDDL to JANI (Dr.-Ing. E.M. Hahn)
A big data approach for fewer train delays (MSc L Jimenez Roa, Prof.dr. M.I.A. Stoelinga, Onno van der Wal (Arcadis))
Supporting Students in their Element (dr. A. Fehnker)
Data-Intensive Software Development without Downtime (Dr. M. van Keulen, prof.dr.ir. A. Rensink)
Consider It Parsed (dr. V Zaytsev)
Verification of distributed algorithms (prof.dr. M. Huisman)
Test First? Before Programming? Seriously? - Integrating software engineering practices in non-software engineering degrees. (dr. A. Fehnker)
Formal Verification of Efficient Data Structures for Web Services to Automotive Lease Companies (dr. S.C.C. Blom, prof.dr. M. Huisman)
Safety verification of Deep Neural Networks for highly automated driving (V.H. Hashemi, Dr.-Ing. E.M. Hahn)
Projects related to Probabilistic Model Checking: Theory, Algorithms, Implementation, Modelling (Dr. A. Hartmanns)
Better maintenance of trains via model checking (Dr. C.E. Budde, Prof.dr. M.I.A. Stoelinga)
Which car should you buy? Analysis of product variations with SAT solving (at BetterBe.com) (Prof.dr. M.I.A. Stoelinga)
Risk Assessment of Water Supply Networks (Prof.dr. M.I.A. Stoelinga, MSc L Jimenez Roa)

Creative

Creative Technology

Supporting Students in their Element (dr. A. Fehnker)

Dependability, security and performance

Analysis of dependability, security and quantitative aspects.

Translating RDDL to JANI (Dr.-Ing. E.M. Hahn)
Security verification of internet protocol implementations (prof.dr. M. Huisman, Aiko Pras)
A big data approach for fewer train delays (Prof.dr. M.I.A. Stoelinga, Onno van der Wal (Arcadis), MSc L Jimenez Roa)
Automated security verification of code for embedded devices (prof.dr. M. Huisman, R. Krak)
Data-Intensive Software Development without Downtime (prof.dr.ir. A. Rensink, Dr. M. van Keulen)
Safety verification of Deep Neural Networks for highly automated driving (Dr.-Ing. E.M. Hahn, V.H. Hashemi)
Speeding up simulation of fault trees (Prof.dr. M.I.A. Stoelinga, Dr. C.E. Budde)
Projects related to Probabilistic Model Checking: Theory, Algorithms, Implementation, Modelling (Dr. A. Hartmanns)
Finding good state elimination orders (Dr.-Ing. E.M. Hahn)
JANI for the web (Dr.-Ing. E.M. Hahn)

Graphs

Graph and graph transformation related research.

Parity game algorithms (T. van Dijk)
Verification of (parallel) model checking algorithms (prof.dr. M. Huisman)
Projects related to Probabilistic Model Checking: Theory, Algorithms, Implementation, Modelling (Dr. A. Hartmanns)
Graph algorithms for theorem (dis)proving (prof.dr.ir. H.J. Broersma)
Risk Assessment of Water Supply Networks (Prof.dr. M.I.A. Stoelinga, MSc L Jimenez Roa)
Finding good state elimination orders (Dr.-Ing. E.M. Hahn)

Languages

Formal languages for specification, modelling and programming.

Translating RDDL to JANI (Dr.-Ing. E.M. Hahn)
Incremental Testing of VerCors (prof.dr. M. Huisman)
Automatic annotation generation for barriers on GPUs: From GPUVerify to VerCors (prof.dr. M. Huisman, M. Safari)
Projects related to Probabilistic Model Checking: Theory, Algorithms, Implementation, Modelling (Dr. A. Hartmanns)

Logics and semantics

Program logics, Semantics, Temporal and Modal logics.

Deductive Verification for LLVM-IR ()
Parity game algorithms (T. van Dijk)
Verification of (parallel) model checking algorithms (prof.dr. M. Huisman)
Verification of distributed algorithms (prof.dr. M. Huisman)
Verification of Software for Embedded Systems (prof.dr. M. Huisman, Prof.Dr. P. Herber)
Projects related to Probabilistic Model Checking: Theory, Algorithms, Implementation, Modelling (Dr. A. Hartmanns)
Verification of Concurrent Software (prof.dr. M. Huisman)
Which car should you buy? Analysis of product variations with SAT solving (at BetterBe.com) (Prof.dr. M.I.A. Stoelinga)

Software Technology

Test coverage, Software Desgin patterns, Software Modeling, Software Architecture.

Supporting Students in their Element (dr. A. Fehnker)
Master projects at Ortec Finance (M. Seijbel, prof.dr. M. Huisman)
Data-Intensive Software Development without Downtime (Dr. M. van Keulen, prof.dr.ir. A. Rensink)
Consider It Parsed (dr. V Zaytsev)
Test First? Before Programming? Seriously? - Integrating software engineering practices in non-software engineering degrees. (dr. A. Fehnker)
Master projects at XSens (prof.dr. M. Huisman)
Graduation Assignment PolderValley (prof.dr. M. Huisman)
Safety verification of Deep Neural Networks for highly automated driving (V.H. Hashemi, Dr.-Ing. E.M. Hahn)
Project proposals at TNO ()
Master projects at Info Support ()
Which car should you buy? Analysis of product variations with SAT solving (at BetterBe.com) (Prof.dr. M.I.A. Stoelinga)

Testing

Formal testing techniques.

Quiescence in Timed Automata (D. van der Wal, Prof.dr. M.I.A. Stoelinga)
Incremental Testing of VerCors (prof.dr. M. Huisman)
Test First? Before Programming? Seriously? - Integrating software engineering practices in non-software engineering degrees. (dr. A. Fehnker)
Test coverage for GPU kernels (B. van Werkhoven, prof.dr. M. Huisman)

Other

Projects that don't fit any other category

Empirical Study on Design by Contract Teaching (Dr. R.E. Monti, prof.dr. M. Huisman)
Case studies in model based testing of statistical behaviour (Dr. M. Gerhold, Prof.dr. M.I.A. Stoelinga)
Modeling medical protocols with UPPAAL (dr.ir. R. Langerak)

In Progress

Dennis Aanstoot - Graph Rewriters as Components
Antoine Veenstra - Acceleration of Combinatorial testing using GPGPU.
Martijn Renssen - Floating Point Axiomatisation for VerCors
Rick de Vries - Clash of Clangs
Bui Hong Thien Nhat - Improvise. Adapt. Overcome. Transform.
Ramesh Krishnamurthy - Formal verification of a distributed control software implemented in the ADA programming language through model checking
Pieter Bos - Program Verification for Quantum Algorithms
Han Hollander - Verification of Set-based Strongly-Connected Components algorithms in VerCors
Samarjeet Patil - Automated Vulnerability detection in Java Source Code using Graph Neural Network
Jan Boerman - Verification of opacity for a transactional memory implementation

Completed

Hans van der Laan - Incremental verification of physical access control systems (January 2021)
René Boschma - Exploring the World of Container Stacking using Approximate Dynamic Programming (November 2020)
Sven Konings - Code Quality Analysis when Mixing Functional and Object-Oriented Programming in Scala (November 2020)
Michiel Bakker - Model validation for Stochastic Timed Automata (August 2020)
Damiano Sartori - Redactable Blockchain - How to change the immutable and the consequences of doing so (August 2020)
Tim Kemp - An algorithmic approach to a conjecture of Chvátal on toughness and hamiltonicity of graphs (August 2020)
Marijn Peppelman - Encoding failure probability dependencies in Bayesian networks (August 2020)
Joran Honig - Incremental Symbolic Execution (June 2020)
Patrick Thijssen - OCL Made Easy (June 2020)
Lukas Miedema - QuickInterp - JIT-like performance in a cross-platform cross-CPU way (June 2020)
Jochem Harmes - A threat model analysis of audio recording on mobile health care applications (June 2020)
Bob Rubbens - Improving Support for Java Exceptions and Inheritance in VerCors (May 2020)
Ömer Sakar - Support for ADTs in VerCors (April 2020)
Bram Kamies - A Generic Framework for State Space Exploration (March 2020)
Steven de Heus - A parity game game (March 2020)
Wybren Kortstra - Aligning Medical Data using Model Transformation (January 2020)
Danny Bergsma - Porting tree-based hash table compression to GPGPU model checking (December 2019)
Remco de Man - Provaby Correct Graph Models (December 2019)
Sjoerd Wels - Guaranteed-TX: The exploration of a guaranteed cross-shard transaction execution protocol for Ethereum 2.0 (October 2019)
Rob Stortelder - Enabling Centralized Access to a Reactive Architecture for Hardware Control Systems (September 2019)
Ruben Haasjes - Metamodel Transformations Between UML and OWL (August 2019)
Indrek Klanberg - A discrete model for neuronal network dynamics (August 2019)
Willem Siers - Synthesizing transformations between APIs (August 2019)
Tim Sonderen - A Manual for Attack Trees (July 2019)
Roman Wiedijk - Code-instrumentation with MOD-BEAM (July 2019)
Henk Mulder - Performance of program verification with Vercors (July 2019)
Jochem Schutte - Design of a development platform to monitor andmanage Low Power, Wide Area WSNs (June 2019)
Rob van Emous - Towards Systematic Black-Box Testing for Exploitable Race Conditions in Web Apps (June 2019)
Remco Brunsveld - Determining the Satisfiability of Car Configuration Models in a Repetitive Manner (May 2019)
Tim Blok - ZITA - A self learning tutoring assistant (May 2019)
Minh Nguyen - Formal verification of a red-black tree data structure (March 2019)
Ramon Onis - Does your model make sense? Automated validation of timed automata (December 2018)
Lars Stegeman - Runtime Monitoring of Smart Contracts on Ethereum (November 2018)
Matthijs Hofstra - Loop invariant generation (November 2018)
Ivaylo Hristov - System for improving analysis of complexes in real estate asset management (September 2018)
Sophie Lathouwers - Formal Verification of Sanitizers (September 2018)
Mart Oude Weernink - Developing a system for the integration of vehicle data (August 2018)
Martijn Willemsen - Improving diagnosis by Grouping Test Cases to Reduce Complexity (July 2018)
Djurre van der Wal - Translating AWN networks to the mCRL2 model checker (En route to formal routing protocol development) (July 2018)
Djurre van der Wal - Verification of Wireless Network Protocols (AWN) (July 2018)
Peter Wessels - Leveraging Behavioural Domain Models in Model-Driven User Interface Development with GLUI (July 2018)
Peter van Dijk - An efficient simulation of crosslinked RAFT copolymerization (June 2018)
Jan-Jelle Kester - CheckMerge: A System for Risk Assessment of Code Merges (April 2018)
Mark Meijerink - A visual DSL for automating business processes (April 2018)
Sebastiaan La Fleur - Formal Verification of Rebel Specifications (March 2018)
Thijs Wiefferink - Combining usage and profile data for retrospectively analyzing usability of applications with funnels (March 2018)
Twan Coenraad - Improved static type inference for Ruby (February 2018)
Folmer Heikamp - Gray-box Network Fuzzing using Genetic Algorithms and Code Coverage (January 2018)
J. Spel - Monotonicity in Markov Chains (January 2018)
Lennart Buit - Domain-specific language for light control queries (November 2017)
Janina Torbecke - Symbolic Model Checking with Partitioned BDDs in Distributed Systems (September 2017)
Tanja de Jong - Using Requirement Templates to Automate Requirements Formalization (August 2017)
Roeland Krak - Cycle-Accurate Timing Channel Analysis of Binary Code (May 2017)
Thom Ritterfeld - On-Demand App Development (December 2016)
Richard Heijblom - Using Features Of Models To Improve State Space Exploration (December 2016)
Rick Hindriks - Vulnerability Analysis of Cyber Security Modelling Language models using Probabilistic Logic (December 2016)
Jelte Zeilstra - A logic to reason about distributed programs (November 2016)
Sybe van Hijum - Symbolic Model Checking of Timed Automata (September 2016)
Jochem Elsinga - Go to Your Graph: Best-First Search in Graph Transformation (August 2016)
Jeroen Vonk - Bisimulation Reduction with MapReduce (August 2016)
Thomas Neele - GPU implementation of Partial-Order Reduction (July 2016)
Ale Strooisma - A monitoring solution for multi-language software (July 2016)
Gert Jan Laverman - Java Code Virtualization of Industrial-strength Java Code (July 2016)
Jenny den Ouden - A quest for the best automated tests: Estimating software reliability based on Spec Explorer's on-the-fly test results (May 2016)
David Huistra - Automated Generation of Attack Trees (March 2016)
Niels Wolters - Quantitative analysis of attack trees with timed automata (March 2016)
Roland Balk - SQLento: Database programming made easier (January 2016)
Charl de Leur - Permission-based separation logic for Scala (August 2015)
Stijn Gijsen - Runtime checking of concurrent Java programs using permissions (August 2015)
Alessio Parzian - Java Card Bytecode Verification (August 2015)
Wytse Oortwijn - Distributed Symbolic Reachability Analysis (July 2015)
Damiaan van der Kruk - A Domain-Specific Language for Specifying Distributed Real-Time Software System Configurations (June 2015)
Vincent Bloemen - On-The-Fly Parallel Decomposition of Strongly Connected Components (June 2015)
Jeroen Thunnissen - Communication software for ICU patients (May 2015)
Jurgen Kleverwal - Supervised Text Classification of Medical Triage Reports (April 2015)
Atze Bouius - Characterizing the Ripple Effects of Introducing Energy-Awareness Functionality in Cyber-Physical-Systems Software (January 2015)
Dennis Windhouwer - The Modularity of the Resource Utilization Model in Python (December 2014)
Maryam Haji Ghasemi - Symbolic Model Checking using Zero-suppressed Decision Diagrams (December 2014)
Jorne Kandziora - Runtime checking of multithreaded programs (August 2014)
Vincent Weber - UTFM - a Next Generation Language and Tool for Feature Modeling (August 2014)
Ivo van Hurne - Towards a Unifying Framework for Modelling and Executing Model Transformations (June 2014)
Jeroen Meijer - Improving Reachability Analysis in LTSmin (March 2014)
Roel ter Maat - A Framework for Modular Implementation of Domain-Specific Event-Based Applications (March 2014)
Ruud Welling - Conflict Detection and Analysis for Single-Pushout High-Level Replacement (February 2014)
Sandra Drenthen - Towards Continuous Delivery in System Integration Projects (February 2014)
Maks Verver - A Framework for Experimentation with Parity Games (December 2013)
Marije de Heus - Design and evaluation of a recommender system for high school courses in The Netherlands (December 2013)
Freark van der Berg - Model checking LLVM using LTSmin (December 2013)
Shirin Zarghami - Middleware for Internet of Things (November 2013)
Richard Cornelissen - Towards a Methodology-Growing Framework (November 2013)
Ferry Olthuis - A comparison of state space reduction techniques in SCOOP (September 2013)
Julien Hemono - Learning Memory Models (September 2013)
Jelmer ter Wal - Java Collections API Specifications in JML (September 2013)
Björn Postma - Fluid Survival Tool: A model checker for Hybrid Petri nets (August 2013)
Daan van Beek - Comparing the LTSmin and NuSMV reachability tools via automatic translation of their respective input languages (August 2013)
Marnix van 't Riet - Trace-based debugging for Advanced-Dispatching programming languages (August 2013)
Marijn Schuurman - Cloud infrastructure at Hydrologic (May 2013)
Vincent de Bruijn - Model-based testing with graph transformations (April 2013)
Rob Bamberg - Non-Deterministic Generalised Stochastic Petri Nets -- Modelling and Analysis (November 2012)
Thijs ten Hoeve - Model Based Testing of a PLC Based Interlocking System (November 2012)
Harold Bruintjes - Bridging GROOVE to the world using an abstracted language model (November 2012)
Ronald Burgman - Partial-order reduction in a dynamic context (October 2012)
Lesley Wevers - A Persistent Functional Language for Concurrent Transaction Processing (August 2012)
Gerjan Stokkink - Quiescent Transition Systems (August 2012)
Bart Postma - AADL Modelling and Analysis of Dependable Space Systems (August 2012)
Ruben Oostinga - A Java Bridge for LTSmin (July 2012)
Tom van Dijk - Parallel implementation of BDD operations for model checking (April 2012)
Tien-Loong Siaw - Saturation for LTSmin (February 2012)
Erik Hegeman - On the Quality of Quality models (July 2011)
Elwin Pater - Partial Order Reduction for PINS (May 2011)
Martijn Adolfsen - Industrial Validation of Test Coverage Quality (March 2011)
Erik Slomp - Reducing UPPAAL models through control flow analysis (September 2010)
Stefan Teijgeler - Connecting Groove to the World using XMI (August 2010)
Gijs Kant - Distributed State Space Generation for Graphs up to Isomorphism (August 2010)
Olaf Keijsers - Extending the Groove Control Language with variables (June 2010)
Jan Scherer - An Eclipse-Based Debugger for Embedded Systems Software (April 2010)
Alex Admiraal - Automated ANTLR Treewalker Generation (February 2010)
Matthijs Ooms - Provenance Management in Practice (September 2009)
Wim J. Bos - Interactive Signaling Network Analysis Tool (August 2009)
Wouter M. Everse - Modelling and Verification of a Shortest Path Tree Protocol (July 2009)
Richard Rietema - Automatic Verification and Analysis of Test Results of Océ Printers (May 2009)
Berteun Damman - Representing PCTL Counterexamples (December 2008)
Marc de Jonge - The SpinJ Model Checker (September 2008)
Jeroen Mengerink - SeCo - A Tool for Semantic Test Coverage (August 2008)
Frank J. van Es - Type Inference for Graph Transformation Systems (July 2008)
Mark Timmer - Evaluating and Predicting Actual Test Coverage (June 2008)
Paul F.Th. Zandbergen - A Bayesian network reliability software tool (May 2008)
Viet Yen Nguyen - Optimising Techniques for Model Checkers (December 2007)
Jeroen van Yperen - SPEX: A Simple Promela EXplorer for TorX (November 2007)
Riemer van Rozen - A Debugging Framework for NIPS (October 2007)
Niels H.M. Aan de Brugh - Software Model Checking for Mono (September 2007)
Jan-Hendrik Kuperus - Nested Quantification in Graph Transformation Rules (June 2007)
Niek Sombekke - Graph-Based Semantics of the .NET Intermediate Language (May 2007)
H.A. (Marcel) Oldenkamp - Probabilistic model checking: a comparison of tools (May 2007)
Arend E. van Putten - Behavioural Hybrid Process Calculus - Translation to Modelica (May 2007)
Emond Papegaaij - The Tree Processing Language (March 2007)
Ivo J. ter Horst - Performance Evaluation in an Early Development Phase (February 2007)
Pepijn Crouzen - Compositional Analysis of Dynamic Fault Trees using IOIMCs (December 2006)
Mark A. Kattenbelt - Towards an Explicit-State Model Checking Framework (September 2006)
M. Helen Schonenberg - Bhave! - Discrete Simulation of Behavioural Hybrid Process Calculus (September 2006)
Tim Kemna - Bisimulation Minimisation and Probabilistic Model Checking (August 2006)
Johan Gorter - Modeling and Analysis of the Liveness UPnP Extension (April 2006)
Jasper K. Berendsen - Reachability in Weighted Probabilistic Timed Automata (December 2005)
Bas V.J.M. Huisman - Formal Analysis and Comparison of Siemens' DIS based architectures (August 2004)
Maneesh Khattri & Mhd. Reza M. I. Pulungan - Model Checking Markov Reward Models with Impulse Rewards (June 2004)
Michèl A.J. Rosien - Design and Implementation of a Systematic State Explorer (March 2001)