Methods and Tools for Verification (MTV)
From the year 2017-2018, the MTV Master programme will be discontinued.
Within the Master programme "Methods and Tools for Verification (MTV)" students become acquainted with a broad range of formal verification and validation techniques and tools, and the theory underlying these. This combination of providing a broad view on the field of formal methods, together with an in-depth understanding of their working makes this a unique program that is of interest to anybody who wishes to understand how to develop reliable software.
The MTV programma is a specialization within the Computer Science (CS) Master programme of the University of Twente. The Formal Methods and Tools (FMT) group is responsible for the programme. It is closely related to the CTIT research theme Dependable Systems and Networks (DSN), and to the graduate programme Dependable and Secure Computing .
The MTV Master is targeted towards ambitious computer science students, who want to become
- validation engineers, who know a broad range of validation techniques and tools, and know when and how to apply these techniques and tools within a system's life cycle, and/or
- researchers, who want to do theoretical and foundational research in the realm of formal methods, and/or
- tool builders, who are able to implement formal theories into working tools, which then can assist system- and validation engineers in developing correct systems.
The attainment levels for the MTV programme give an overview of the capabilities of a MTV graduate.
To enroll in the MTV Master Programme, you have to fill in a course programme in agreement with the MTV programme mentor Prof. Dr. Marieke Huisman, and hand it in at the Educational Administration (BOZ).
The course programme form for 2016-2017 is available here.
For any questions about the MTV programme, please contact Prof. Dr. Marieke Huisman.
The following subjects are mandatory. They are basic and broad, and are also of importance for other, non-MTV CS specialization themes (e.g. SE or ES).
|192111092||Advanced Logic||..3.||Arend Rensink|
|192135310||Modelling and Analysis of Concurrent Systems 1||1...||Rom Langerak / Jaco van de Pol|
|192140122||System Validation||1...||Marieke Huisman|
|192170015||Testing Techniques||..3.||Mariëlle Stoelinga|
At least 20 EC of the following courses:
|192135450||ADSA-Model Driven Engineering||.2..||Luis Ferreira Pires|
|201400170||Best practices in software development||...4||Ansgar Fehnker|
|201400200||Capita selecta for MTV||1234|
|201400173||Concepts in programming languages||.2..||Mehmet Aksit|
|191210430||Engineering System Dynamics (Dynamische Systemen)||.2..||Peter Breedveld/ Jan Broenink / Raffaella Carloni|
|192130092||Fault tolerant digital systems||1...||Hans Kerkhoff|
|191520751||Graph theory||..3.||Harry Aarts/ Walter Kern|
This course replaces Mathematical Programming.
|192620300||Performance evaluation||.2..||Boudewijn Haverkort|
|201200006||Quantitative Evaluation of Embedded Systems||.2..||Anne Remke|
|201600040||Requirements Engineering Processes and Methods||.2..||Maya Daneva|
|201600051||Software Security||.2..||Jaco van de Pol|
|191561560||Systems and Control||1-2..||Jan Willem Polderman|
At least 3 of the following courses:
|192135320||Modelling and Analysis of Concurrent Systems 2||...4||Jaco van de Pol|
|192114300||Program Verification||...4||Marieke Huisman|
|201300042||Limits to Computing||1...||Bodo Manthey|
|191581420||Optimization Modelling||..3.||Bodo Manthey|
|192114100||Principles of Model Checking
This course is lectured only every second year. It will be lectured in 2016 - 2017.
We recommend you to do a traineeship (= internship or 'stage', 192199968, 20 credits). If you do not choose a traineeship, we suggest that you define an individual project where the verification techniques and tools are applied on a realistic example.
Academic and Organizational Skills
Moreover, the student may choose 0 to 10 ECTS courses from the following list, or any other appropriate course that will help to further develop academic and organizational skills, in agreement with the programme mentor.
|201200009||Managing Change & Human Resources|
|201000260||Advanced Science Communication|
There is an overview of open, current and completed Master projects within the FMT chair.
Domain specific attainment levels for MTV
Apart from the general attainment levels for the CS Master, MTV graduates demonstrate their specialist knowledge as follows.
- MTV graduates have a thorough knowledge of and understand the scope of formal methods as a scientific and design discipline.
- MTV graduates have a thorough knowledge of, understand and gain practical experience with the application of formal methods and tools in the development process of software, distributed and/or embedded systems.
- MTV graduates can apply formal methods and tools during system development on the basis of knowledge and insight, make an informed selection of these and contribute to their further development.
- MTV graduates have a knowledge of and understand various aspects of theoretical computer science, including process algebra, proof systems and formal testing theory.
- MTV graduates have specialist knowledge and understanding of one or more sub-fields or aspects of the formal methods discipline, e.g. Process Algebra, Software Model Checking, Distributed Model Checking, Program Verification, Proof Systems, Testing, Quantitative Modelling and/or Analysis, Graph Transformations, Game Theory.
- MTV graduates have practical experience conducting scientific research into formal methods, contribute to such research, apply the results, follow the trends of this sub-field and contribute to its further development.
Relation with other Master programmes
Apart from its own foundational research, formal methods are focused on assisting other computer science fields in the design and implementation of reliable and dependable (software) systems. It is therefore no coincidence that the FMT group closely works together with other research groups that strive for dependable systems.
Consequently, FMT is also present in other Master programmes that are concerned with the development of reliable systems:
- Software Technology (ST) track of the CS Master programme
- Embedded Systems (ES) , 3TU Master programme
- Telematics Master programme
Within these Master programmes there are possibilities to follow a MTV/FMT line that ends in a Master project at FMT.