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. Marieke Huisman, the study advisor of FMT.

Available

Algorithms and Data Structures

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

Improved PROMELA BEEMing (contact: prof.dr. J.C. van de Pol & A.W. Laarman MSc)
Learning Memory Models (contact: dr. M. Huisman)
Permission-based separation logic for concurrent Scala programs (contact: dr. M. Huisman & dr. S.C.C. Blom)
Use of permission-based separation logic to specify multi-threaded applications (contact: dr. M. Huisman)

Case studies and Applications

Application of formal methods to practical examples.

Cloud infrastructure at Hydrologic (contact: dr. M.I.A. Stoelinga)
Improving Efficiency within Health Care Organizations (contact: dr. M.I.A. Stoelinga)
Java Collections API Specifications in JML (contact: dr. W.I. Mostowski & dr. M. Huisman & dr. S.C.C. Blom)
Test Coverage Using Industrial Case Studies (contact: M. Timmer MSc & dr. M.I.A. Stoelinga)
Using model-based techniques for integration of subsystems (contact: dr.ir. G.J. Tretmans)

Dependability, security and performance

Analysis of dependability, security and quantitative aspects.

Graphs

Graph and graph transformation related research.

Converting graph transformations between GROOVE and RDT (contact: prof.dr.ir. A. Rensink)
Ensuring Safe Model Transformation (contact: prof.dr.ir. A. Rensink & dr. M.J. de Mol & dr. M. Huisman)
Faster Large-Model Transformation (contact: dr. M.J. de Mol & prof.dr.ir. A. Rensink)
How to Get to Your Graph (contact: prof.dr.ir. A. Rensink & dr. A.H. Ghamarian)

Languages

Formal languages for specification, modelling and programming.

Code generation from UPPAAL to Real-Time Java (contact: prof.dr.ir. A. Rensink & dr. M.I.A. Stoelinga)
Converting graph transformations between GROOVE and RDT (contact: prof.dr.ir. A. Rensink)
Generation of JML annotations for the static verification of security automata (contact: dr. M. Huisman)
Java Collections API Specifications in JML (contact: dr. W.I. Mostowski & dr. M. Huisman & dr. S.C.C. Blom)

Logics and semantics

Program logics, Semantics, Temporal and Modal logics.

Algorithmic techniques for Compositional Verification (contact: dr. M. Huisman)
Learning Memory Models (contact: dr. M. Huisman)
OCL Made Easy (contact: prof.dr.ir. A. Rensink & Kurtev)
Permission-based separation logic for concurrent Scala programs (contact: dr. M. Huisman & dr. S.C.C. Blom)
Use of permission-based separation logic to specify multi-threaded applications (contact: dr. M. Huisman)

Testing

Formal testing techniques.

Test Coverage Using Industrial Case Studies (contact: M. Timmer MSc & dr. M.I.A. Stoelinga)

In Progress

Bart Postma - AADL Modelling and Analysis of Dependable Space Systems
Gerjan Stokkink - Time in untimed testing
Lesley Wevers - A Functional Database Programming Language
Maks Verver - A Framework for Experimentation with Parity Games
Rob Bamberg - Combining forces in model checking
Ruben Oostinga - A Java Bridge for LTSmin
Vincent de Bruijn - Model-based testing with graph transformations

Completed

Parallel implementation of BDD operations for model checking - Tom van Dijk (Apr 2012)
Saturation for LTSmin - Tien-Loong Siaw (Feb 2012)
On the Quality of Quality models - Erik Hegeman (Jul 2011)
Partial Order Reduction for PINS - Elwin Pater (May 2011)
Industrial Validation of Test Coverage Quality - Martijn Adolfsen (Mar 2011)
Reducing UPPAAL models through control flow analysis - Erik Slomp (Sep 2010)
Connecting Groove to the World using XMI - Stefan Teijgeler (Aug 2010)
Distributed State Space Generation for Graphs up to Isomorphism - Gijs Kant (Aug 2010)
Extending the Groove Control Language with variables - Olaf Keijsers (Jun 2010)
An Eclipse-Based Debugger for Embedded Systems Software - Jan Scherer (Apr 2010)
Automated ANTLR Treewalker Generation - Alex Admiraal (Feb 2010)
Provenance Management in Practice - Matthijs Ooms (Sep 2009)
Interactive Signaling Network Analysis Tool - Wim J. Bos (Aug 2009)
Modelling and Verification of a Shortest Path Tree Protocol - Wouter M. Everse (Jul 2009)
Automatic Verification and Analysis of Test Results of Océ Printers - Richard Rietema (May 2009)
Representing PCTL Counterexamples - Berteun Damman (Dec 2008)
The SpinJ Model Checker - Marc de Jonge (Sep 2008)
SeCo - A Tool for Semantic Test Coverage - Jeroen Mengerink (Aug 2008)
Type Inference for Graph Transformation Systems - Frank J. van Es (Jul 2008)
Evaluating and Predicting Actual Test Coverage - Mark Timmer (Jun 2008)
A Bayesian network reliability software tool - Paul F.Th. Zandbergen (May 2008)
Optimising Techniques for Model Checkers - Viet Yen Nguyen (Dec 2007)
SPEX: A Simple Promela EXplorer for TorX - Jeroen van Yperen (Nov 2007)
A Debugging Framework for NIPS - Riemer van Rozen (Oct 2007)
Software Model Checking for Mono - Niels H.M. Aan de Brugh (Sep 2007)
Nested Quantification in Graph Transformation Rules - Jan-Hendrik Kuperus (Jun 2007)
Graph-Based Semantics of the .NET Intermediate Language - Niek Sombekke (May 2007)
Behavioural Hybrid Process Calculus - Translation to Modelica - Arend E. van Putten (May 2007)
Probabilistic model checking: a comparison of tools - H.A. (Marcel) Oldenkamp (May 2007)
The Tree Processing Language - Emond Papegaaij (Mar 2007)
Performance Evaluation in an Early Development Phase - Ivo J. ter Horst (Feb 2007)
Compositional Analysis of Dynamic Fault Trees using IOIMCs - Pepijn Crouzen (Dec 2006)
Towards an Explicit-State Model Checking Framework - Mark A. Kattenbelt (Sep 2006)
Bhave! - Discrete Simulation of Behavioural Hybrid Process Calculus - M. Helen Schonenberg (Sep 2006)
Bisimulation Minimisation and Probabilistic Model Checking - Tim Kemna (Aug 2006)
Modeling and Analysis of the Liveness UPnP Extension - Johan Gorter (Apr 2006)
Reachability in Weighted Probabilistic Timed Automata - Jasper K. Berendsen (Dec 2005)
Formal Analysis and Comparison of Siemens' DIS based architectures - Bas V.J.M. Huisman (Aug 2004)
Model Checking Markov Reward Models with Impulse Rewards - Maneesh Khattri & Mhd. Reza M. I. Pulungan (Jun 2004)
Design and Implementation of a Systematic State Explorer - Michèl A.J. Rosien (Mar 2001)

	FMT Home > Education > MSc Projects
<< EEMCS (EWI) Home News In the Media Research Education » Courses » MTV Master » Graduate School » BSc Projects » MSc Projects » Design Projects » Internships People Events Vacancies Internal Contact	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. Marieke Huisman, the study advisor of FMT. Available Algorithms and Data Structures Correct and efficient algorithms and datastructures for concurrency and model checking. Improved PROMELA BEEMing (contact: prof.dr. J.C. van de Pol & A.W. Laarman MSc) Learning Memory Models (contact: dr. M. Huisman) Permission-based separation logic for concurrent Scala programs (contact: dr. M. Huisman & dr. S.C.C. Blom) Use of permission-based separation logic to specify multi-threaded applications (contact: dr. M. Huisman) Case studies and Applications Application of formal methods to practical examples. Cloud infrastructure at Hydrologic (contact: dr. M.I.A. Stoelinga) Improving Efficiency within Health Care Organizations (contact: dr. M.I.A. Stoelinga) Java Collections API Specifications in JML (contact: dr. W.I. Mostowski & dr. M. Huisman & dr. S.C.C. Blom) Test Coverage Using Industrial Case Studies (contact: M. Timmer MSc & dr. M.I.A. Stoelinga) Using model-based techniques for integration of subsystems (contact: dr.ir. G.J. Tretmans) Dependability, security and performance Analysis of dependability, security and quantitative aspects. Comparison of Formalisms for Dependability (contact: dr. M.I.A. Stoelinga) Generation of JML annotations for the static verification of security automata (contact: dr. M. Huisman) Quantitative Analysis of Secure Information Flow for Multi-threaded Programs (contact: dr. M. Huisman & M.T. Ngo MSc) Graphs Graph and graph transformation related research. Converting graph transformations between GROOVE and RDT (contact: prof.dr.ir. A. Rensink) Ensuring Safe Model Transformation (contact: prof.dr.ir. A. Rensink & dr. M.J. de Mol & dr. M. Huisman) Faster Large-Model Transformation (contact: dr. M.J. de Mol & prof.dr.ir. A. Rensink) How to Get to Your Graph (contact: prof.dr.ir. A. Rensink & dr. A.H. Ghamarian) Languages Formal languages for specification, modelling and programming. Code generation from UPPAAL to Real-Time Java (contact: prof.dr.ir. A. Rensink & dr. M.I.A. Stoelinga) Converting graph transformations between GROOVE and RDT (contact: prof.dr.ir. A. Rensink) Generation of JML annotations for the static verification of security automata (contact: dr. M. Huisman) Java Collections API Specifications in JML (contact: dr. W.I. Mostowski & dr. M. Huisman & dr. S.C.C. Blom) Logics and semantics Program logics, Semantics, Temporal and Modal logics. Algorithmic techniques for Compositional Verification (contact: dr. M. Huisman) Learning Memory Models (contact: dr. M. Huisman) OCL Made Easy (contact: prof.dr.ir. A. Rensink & Kurtev) Permission-based separation logic for concurrent Scala programs (contact: dr. M. Huisman & dr. S.C.C. Blom) Use of permission-based separation logic to specify multi-threaded applications (contact: dr. M. Huisman) Testing Formal testing techniques. Test Coverage Using Industrial Case Studies (contact: M. Timmer MSc & dr. M.I.A. Stoelinga) In Progress Bart Postma - AADL Modelling and Analysis of Dependable Space Systems Gerjan Stokkink - Time in untimed testing Lesley Wevers - A Functional Database Programming Language Maks Verver - A Framework for Experimentation with Parity Games Rob Bamberg - Combining forces in model checking Ruben Oostinga - A Java Bridge for LTSmin Vincent de Bruijn - Model-based testing with graph transformations Completed Parallel implementation of BDD operations for model checking - Tom van Dijk (Apr 2012) Saturation for LTSmin - Tien-Loong Siaw (Feb 2012) On the Quality of Quality models - Erik Hegeman (Jul 2011) Partial Order Reduction for PINS - Elwin Pater (May 2011) Industrial Validation of Test Coverage Quality - Martijn Adolfsen (Mar 2011) Reducing UPPAAL models through control flow analysis - Erik Slomp (Sep 2010) Connecting Groove to the World using XMI - Stefan Teijgeler (Aug 2010) Distributed State Space Generation for Graphs up to Isomorphism - Gijs Kant (Aug 2010) Extending the Groove Control Language with variables - Olaf Keijsers (Jun 2010) An Eclipse-Based Debugger for Embedded Systems Software - Jan Scherer (Apr 2010) Automated ANTLR Treewalker Generation - Alex Admiraal (Feb 2010) Provenance Management in Practice - Matthijs Ooms (Sep 2009) Interactive Signaling Network Analysis Tool - Wim J. Bos (Aug 2009) Modelling and Verification of a Shortest Path Tree Protocol - Wouter M. Everse (Jul 2009) Automatic Verification and Analysis of Test Results of Océ Printers - Richard Rietema (May 2009) Representing PCTL Counterexamples - Berteun Damman (Dec 2008) The SpinJ Model Checker - Marc de Jonge (Sep 2008) SeCo - A Tool for Semantic Test Coverage - Jeroen Mengerink (Aug 2008) Type Inference for Graph Transformation Systems - Frank J. van Es (Jul 2008) Evaluating and Predicting Actual Test Coverage - Mark Timmer (Jun 2008) A Bayesian network reliability software tool - Paul F.Th. Zandbergen (May 2008) Optimising Techniques for Model Checkers - Viet Yen Nguyen (Dec 2007) SPEX: A Simple Promela EXplorer for TorX - Jeroen van Yperen (Nov 2007) A Debugging Framework for NIPS - Riemer van Rozen (Oct 2007) Software Model Checking for Mono - Niels H.M. Aan de Brugh (Sep 2007) Nested Quantification in Graph Transformation Rules - Jan-Hendrik Kuperus (Jun 2007) Graph-Based Semantics of the .NET Intermediate Language - Niek Sombekke (May 2007) Behavioural Hybrid Process Calculus - Translation to Modelica - Arend E. van Putten (May 2007) Probabilistic model checking: a comparison of tools - H.A. (Marcel) Oldenkamp (May 2007) The Tree Processing Language - Emond Papegaaij (Mar 2007) Performance Evaluation in an Early Development Phase - Ivo J. ter Horst (Feb 2007) Compositional Analysis of Dynamic Fault Trees using IOIMCs - Pepijn Crouzen (Dec 2006) Towards an Explicit-State Model Checking Framework - Mark A. Kattenbelt (Sep 2006) Bhave! - Discrete Simulation of Behavioural Hybrid Process Calculus - M. Helen Schonenberg (Sep 2006) Bisimulation Minimisation and Probabilistic Model Checking - Tim Kemna (Aug 2006) Modeling and Analysis of the Liveness UPnP Extension - Johan Gorter (Apr 2006) Reachability in Weighted Probabilistic Timed Automata - Jasper K. Berendsen (Dec 2005) Formal Analysis and Comparison of Siemens' DIS based architectures - Bas V.J.M. Huisman (Aug 2004) Model Checking Markov Reward Models with Impulse Rewards - Maneesh Khattri & Mhd. Reza M. I. Pulungan (Jun 2004) Design and Implementation of a Systematic State Explorer - Michèl A.J. Rosien (Mar 2001)