Methods and Tools for Verification (MTV)

From the year 2017-2018, the MTV Master programme will be discontinued.

We refer interested students to the specialisation Software Technology. Information about the new course program for Software Technology should be available soon. For questions, please contact Prof. Dr. Marieke Huisman.


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.

Enrolling

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.

Contact

For any questions about the MTV programme, please contact Prof. Dr. Marieke Huisman.

MTV programme

Basic courses

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).

OSIRIS subject name kw teacher(s)
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

Elective Courses

At least 20 EC of the following courses:

OSIRIS subject name kw teacher(s)
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
201500372 Mathematical Optimization
This course replaces Mathematical Programming.
..3. Walter Kern
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

Advanced courses

At least 3 of the following courses:

OSIRIS subject name kw teacher(s)
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.
1... Joost-Pieter Katoen

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.

201000087 Entrepreneurial Finance
201200009 Managing Change & Human Resources
201000260 Advanced Science Communication
201200148 Study Tour

Mandatory

191612680 Computer Ethics
192199508 Research Topics
192199978 Final Project

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.