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.
Features
|
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. |
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.
| Course | Type | ECTS | University |
Description |
| 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 cryptographic protocols | Optional | 6 | UAM | Cryptography is one of the essential technologies used to ensure data privacy and much more, such as performing secure computations in untrusted environments and ensuring the inmutability of distributed ledgers (e.g., blockchains). |
| 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. |
| 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:
| Monday | Tuesday | Wednesday | Thursday | Friday | |
|---|---|---|---|---|---|
| Fall semester | UCM | UCM | UAM | UAM | UCM |
| Spring semester | UCM | UPM | UPM | UCM |
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.
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).
