Go to content

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

Master Degree on

Formal Methods in Computer Science and Engineering

  at UCM, UPM, and UAM


IMPORTANT: COVID-19 Information

COVID-19 has brought a disruption in normal life during the academic year 2020. This has had an impact on all aspects of society, including higher education. These effects  continue to be felt during 2021. Eeach University is taking different measures according to their characteristics (number of classrooms, their size, schedules, etc.) Since this master is jointly taught by several universities, taking into account their constraints and decisions is necessary.


Some Important Dates for the academic year 2021-2022

  • Advance registration 2021-2022:
    • Not yet announced. Typically from February to end of June.
    • See the UPM official pages for up-to-date-information.
  • List of admissions: not yet announded.
  • Lecture starts:
    • Fall semester: not yet announced.
    • Spring semester: not yet announced.
    • Please check the course pages at UCM and UAM to obtain up-to-date information about their starting dates.

Please consult as well the UPM official webpage to get up-to-date, additional information regarding deadlines to submit additional documentation and other procedures.

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.


Computer systems are nowadays essential and ubiquitous. Most tasks we perform on a daily basis - from driving a car to buying a book - rely on software: we  depend on it and its correct behavior. However, unfortunately, software frequently incurs misbehaviours, often caused by a poor formalization of its design or requirements, or the lack of a rigorous verification of its implementation. This degree aims at presenting techniques to avoid these mistakes and advanced techniques to design, develop, and deploy systems that are cleaner, more resilient, dependable, understandable and maintainable.

This degree aims particularly at computer scientists who are 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, mathematically-rooted tools. Such professionals will successfully accomplish the design and implementation of dependable 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. 
This video (in Spanish) has a short presentation of the master.




Is it for you?

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 level up your skills.

Compañías futuro



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, dependable code is needed by big high-tech companies, banks, social networks, content managers, designers of embedded systems, etc. among many others that require code with guarantees.

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.





First Semester (September-January)


Course Type ECTS University
Static analysis of programs and constraint solving Compulsory 6 UCM 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 UCM Most programs are currently built from the interaction of several execution threads. Understanding  how to model and predict such interactions helps building systems that are correct from the beginning.
Theory of programming languages Compulsory 6 UCM Current mainstream programming languages are more similar to each other than expected. 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 UAM The complexity of modern software can be partially tackled by using domain-specific languages that are able to express certain properties or operations succinctly. Applying 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 UAM In (pre)-history, Nature has faced problems which are similar to computer-related ones (e.g., optimization); in many cases, found solutions whose underlying ideas are quite non-standard emerged. Studying and adapting such solutions leads to the design of techniques that may perform better than standard ones.
Machine learning Optional 6 UAM Big advances in Machine Learning have allowed computers to carry out very complex tasks with satisfactory results. Knowing the foundations and limitations of ML techniques can help in discerning whether an ML-based solution is desirable and gives the expected results.
Design and analysis of security protocols
Optional 6   Currently unavailable
Formal methods for testing Optional 6 UCM Testing is by far the most widely used technique to determine if a program behaves as expected. Although proofs of correctness cannot usually be obtained from testing, it is often the case that formal techniques cannot be applied because of the system complexity or other issues, and therefore testing is the only applicable technique. 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)


Course Type ECTS University Description
Analysis of concurrent and distributed systems Optional 6 UPM 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. Analyzing such aspects requires a number of specific techniques which deserve to be studied in detail.
Design of correct-by-construction systems Optional 6 UPM In order 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 UCM 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 UCM Verifying that a program behaves as expected frequently involves mathematical proofs that are complex, tedious, and error-prone. The use of 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 All Student can get credits for interships in companies or research institutes/groups. An internship 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, internship can have a salary or honorarium associated.
Master's Thesis Compulsory 12 All 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.




During your studies, up to 6 ECTS in the form of internships in tech-related companies or research institutes can be earned. In particular, the IMDEA Software Institute, located in Madrid, often offers short-term internships in research topics close to the masters'.




Lectures take place in three campuses of the participating Universities: Moncloa (UCM), Cantoblanco (UAM), and Montengancedo (UPM) following the scheme below:

Fall semester UCM UCM UAM UAM UCM
Spring semester UCM UPM UPM UCM  


The 2021 spring semester at UPM will start on February 8th and will run up to May 28th.

The UPM global calendar for year 2020-2021 is available here. Note that it may be updated according to the development of COVID-19.


Information on courses given at UPM (Spring Semester)

Correctness by Construction

Static Analysis of Concurrent and Distributed Systems


Teaching staff

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

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




Information about the other Universities involved and other relevant documents