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.
The attainment levels for the MTV programme give an overview of the capabilities of a MTV graduate.

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:

Within these Master programmes there are possibilities to follow a MTV/FMT line that ends in a Master project at FMT.