Back to University of Twente portal
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.
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 |