Methods and Tools for Verification (MTV)
New MTV programme from September 2012
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.
MTV Students
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.
Contact
If you are interested in enrolling into the MTV Master Programme at the FMT group, please contact dr. Marieke Huisman, the programme mentor of the MTV Master programme.MTV programme
Starting September 2012, the official program will be changed. In agreement with the study advisor you can already select courses from the new programme.First Year
The first year of the MTV Master programme has a study load of 60 credits. Of these 60 credits, 35 credits are prescribed below.
FMT base subjects: 4 out 4
In the first year of the MTV master, the following 4 FMT
subjects are mandatory. These four subjects are basic and
broad, and are also of importance for other, non-MTV CS
specialization themes (e.g. SE or ES).
| OSIRIS | subject name | kw | teacher(s) |
| 192111092 | Advanced Logic | ..3. | Rensink |
| 192135310 | Modelling and Analysis of Concurrent Systems 1 | 1... | Langerak / vd Pol |
| 192140122 | System Validation | ...4 | Huisman / Blom |
| 192170015 | Testing Techniques | ..3. | Stoelinga / Brinksma / Timmer / Belinfante |
Other base subjects: 3 out 9
The subject programme must include at least 3 of the following 9 basic subjects.| OSIRIS | subject name | kw | teacher(s) |
| 191520751 | Graph Theory | .2.. | Aarts / Kern |
| 191560561 | Introduction to mathematical systems theory | ...4 | Stoorvogel / Vajta |
| 191580752 | Deterministic models in OR | ..3. | vd Wegen |
| 192111233 | Aspect-oriented Programming | .2.. | Aksit / Bockisch |
| 192111332 | Design of Software Architectures | 1... | Aksit |
| 201100072 | Introduction to Information Security | .2.. | Petkova-Nikova |
| 192620300 | Performance evaluation | .2.. | Remke |
| 192130092 | Faulttolerant digital systems | 1... | Kerkhoff |
| 192130500 | Performance Analysis | .2.. | Remke / Stoelinga |
For the remaining 25 credits, Computer Ethics (191612680, 5 credits, 2nd quarter) is a compulsory subject; the remaining credits are free of choice. We recommend you to do a traineeship (= internship or 'stage', 192199968, 20 credits).
Second Year
The second year of the MTV Master programme has a study load of 60 credits. Of these 60 credits, 20 credits are prescribed (see below) and 40 credits are reserved to the Master project (i.e., Research Topics and the Final Project).FMT advanced subjects: 3 out 4
In the second year of the MTV master, out of the following 4 advanced FMT subjects, 3 have to be chosen.| OSIRIS | subject name | kw | teacher(s) |
| 192114100 | Principles of Model Checking This course will not be lectured in 2011-2012 |
1... | Katoen |
| 192114200 | Quantitative modeling and analysis | .2.. | Stoelinga |
| 192114300 | Program Verification | 1... | Huisman / Rensink |
| 192135320 | Modelling and Analysis of Concurrent Systems 2 | .2.. | vd Pol |
Other advanced subject: 1 out 5
The programme must further include at least 1 of the following 5 subjects.| OSIRIS | subject name | kw | teacher(s) |
| 191210441 | Control engineering | ..3. | Stramigioli |
| 192111700 | Computability and Computational Complexity | 1... | vd Hoeven |
| 192135450 | ADSA Model driven engineering | 1... | Ferreira Pires / Ivanov |
| 192140700 | The numbers tell the tale (meten=weten) | 1... | de Boer / Pras / Remke |
| 192661001 | Patterns for software development | .2.. | Aksit / Bockisch |
Master project
An important part of the second year is reserved to the Master project, which consists of two mandatory parts:| OSIRIS | subject name | credits |
| 192199508 | Research Topics | 10 EC |
| 192199978 | Final Project | 30 EC |
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 Engineering (SE) track of the CS Master programme
- Embedded Systems (ES), 3TU Master programme
- Telematics Master programme