?>

Go to content

Home
ETSIINF en Twitter ETSIINF en Facebook
Inicio > Degree Programmes > Master's degrees > Formal methods in computer science and engineering

structure.html

Interuniversity Master Degree in

Formal Methods in Computer Science

  at UCM, UPM and UAM

Band

Motivation

Important Dates

  • Advance registration 2019: from February 1st to May 31st
  • List of admissions: published on March 15th and June 15th, respectively
  • Deadline to present documents:
    • From Spanish Universities: July 15th
    • From foreign Universities: October 14th

Please look at the UPM official webpage to get up-to-date information.

If you come from a non-EU Country you are strongly advised to apply as soon as possible in order to get your travel VISA on time.

 

REGISTER
 
Nowadays, computer systems are essential and ubiquitous.
Most tasks we perform on a daily basis - from driving a car to buying a book - rely on software; therefore, we certainly depend on it and its correct behavior.
However, unfortunately, software frequently incurs misbehaviors, mostly caused by a poor formalization of its design or requirements, or the lack of a rigorous verification of its implementation.
This Master Degree focuses on advanced techniques to avoid such misbehaviors and deply systems which are cleaner, more resistant, understandable and maintainable.

This Degree is directed to computer scientists who are specially interested in the rigor and trustworthiness of computer systems.

Its main goal is to train professionals who will be able to tackle complex tasks such as assessing software correctness by means of rigorous mathematical tools. Such professionals will successfully devote to the design and implementation of trustworthy code, as well as the validation and verification of third-party software. This Degree also aims at training researchers in Formal Methods.

 
Since it is jointly organized by three public Universities in Madrid (UCM, UPM, UAM), this Master Degree involves as teachers a large corpus of well-known academic researchers. 
 

 








 

Features

Targets

If you have a Degree in Computer Science, Computer Engineering or Mathematics, and you are interested in designing and implementing secure and correct code, this is your place.

Depending on your background, you may be asked to attend additional courses in order to complement your skills.

Compañías futuro

 

Objectives

The use of Formal Methods in Computer Science has become more and more frequent in the last years, due to the growing complexity of computer systems and the need to guarantee that they behave as expected. Trustworthy code is needed by big high-tech companies, banks, social networks, content managers, designers of embedded systems, etc.

Companies and software producers are more and more interested in professionals with a background in Formal Methods.  Likewise, Universities and research institutes are promoting an increasing number of academic positions related to this field.

 

 

 

 

 

Courses

 

First Semester (September-January)

 

Subject Type ECTS Description
Static analysis of programs and constraint solving Compulsory 6 Static program analysis studies properties of programs without the need to execute them: does it terminate? Does it give the expected result? does it have unexpected side effects? It is a powerful tool to guarantee that programs do what they are expected to do... before it's too late.
Concurrency models Compulsory 6 Most programs are currently built from the interaction of several execution threads. To understand the machinery behind such interactions helps building systems which are correct from the beginning.
Theory of programming languages Compulsory 6 Current mainstream programming languages are more similar to each other than expected. To understand their basics is key to tell which features are language-dependent and which are common to all of them.
Formal model-driven software development Optional 6 The complexity of modern software can be partially tackled by using domain-specific languages, which are able to express certain properties succinctly. To apply Formal Methods (program transformation, verification such as model checking or model finding) can help constructing ready-to-use, executable specifications meeting the given requirements.
Design of bio-inspired algorithms Optional 6 In (pre)-history, Nature has faced problems which are similar to computer-related ones (e.g., optimization); in many cases, She found solutions whose underlying ideas are quite non-standard. To study and adapt such solutions leads to the design of techniques that may perform better than standard ones.
Machine learning Optional 6 Lately, big advances in Machine Learning have allowed computers to carry out very complex tasks with satisfactory results. To know the foundations and limitations of ML techniques can help in discerning whether an ML-based solution is reasonable and gives the expected results.
Design and analysis of security protocols
Optional 6 Currently unavailable
Formal methods for testing Optional 6 Testing is by far the most used technique to determined if a program behaves as expected. Although no absolute truth can be obtained by testing, it is often the case that formal techniques cannot be applied because of the system complexity or other issues. When it comes to problem detection, the trustworthiness of testing can be increased if tests are complemented by a formal setting for the creation and validation of test cases.

 

 

Second Semester (February-May)

 

Subject Type ECTS Description
Analysis of concurrent and distributed systems Optional 6 Decomposing a program into several concurrent execution threads which can be run at different locations is becoming more and more common; in this context, the cost of communication (latency, failures, etc.) must be carefully taken into account. To analyze such aspects requires a number of specific techniques which deserve to be studied in detail.
Design of correct-by-construction systems Optional 6 To assess software correctness, one can decompose the verification problem into phases and apply specific techniques to each phase in order to guarantee that the desired requirements are met and the properties proved for the other phases are not broken. This usually involves the use of automatic tools to carry on formal proofs.
Quantum computing Optional 6 The implementation of quantum computing in the real world could dramatically increase the computational power of computer systems, thus paving the way for the solution of (currently) intractable problems or even problems which are not considered as amenable to be solved by means of computers. This course will show the foundations and applications of quantum computing.
Computer-aided program verification Optional 6 To verify that a program behaves as expected frequently involves mathematical proofs which are complex, tedious and error-prone. The use of automatic tools to produce such proofs is key to increase software reliability and the productivity of the software engineer who uses Formal Methods.
Internships in companies or research groups Optional 6 Student can get credits for vacancies in companies of research institutes/groups where they can work on related topics. To do a vacancy can boost the student's skills and help her to apply the newly-acquired knowledge to production or cutting-edge research. Depending of the agreement with the company or research partner, vacancies can be paid.
Master's Thesis Compulsory 12 The Master's Thesis can be directed by any teacher taking part in the Master Degree, regardless of the university she belongs to. It involves autonomous work from the student and a fair amount of innovation.


Timetable for 2018-2019 (please select "MÁSTER MÉTODOS FORMALES")

 

 

 

Vacancies in companies or research institutes/groups

During your studies, you will be recognized up to 6 ECTS in the form of vacancies in tech-related companies or research institutes. In particular IMDEA Software, located in Madrid, will offer short-term internships in closely-related research topics.

 

Teachers

All teachers have been active as researchers in topics related to Formal Methods in the last years; most of them are leading or take part in research projects.

 

Additional information

To enroll at UPM: main steps

This list just resumes the main steps in order to enroll in this Degree an UPM.  Please have a look at the UPM site for complete info. Please consider that you may be asked to provide a different paperwork depending on where you come from.  All documents must be provided either in English or in Spanish (you will need an official translation if you want to present documents in other languages).

  1. Advance Registration: you will need (scanned copy):
  2. Documents are studied by the Degree Board.
  3. The list of admissions is published.  Lists are kept up-to-date during the registration process.
  4. In case of admission, you will receive a letter by email and you will get a student account at UPM.
  5. You will use that letter if you need a travel visa.
  6. After admission, you will enroll in the Degree and choose the subjects you want to attend. You can do it either personally at Escuela Técnica Superior de Ingenieros Informáticos (ETSIINF) or on the Internet.
  7. You will ask for a Carta de Pago (payment document) in order to make the corresponding payment. Afterwards, you will have to present the payment certificate together with the original copy of the documents you presented at the beginning of the process.

 

Contact

 

Information about the other Universities involved

 

Band