The skills acquired during this master’s the program will enable students to apply mathematical methods to the rigorous solution of computing problems. The aim is to train highly qualified professionals to successfully manage the reliable design and deployment of zero-fault systems, their correct implementation, and system assessments or audits to software systems developed by third-parties. The master is also intended to provide basic training for future researchers in formal methods.
Graduates from this program will enhance their capacity to avoid errors caused by inadequate requirement formalization or lack of implementation verification, and will be introduced to the design of systems and programs which are error-free, more robust, and easier to understand and verify. They will thus become highly qualified professionals who can tackle very complex computing problems devising highly dependable solutions. These problems appear in advanced technology sectors which design or maintain the software in fields including telecommunications, air transportation, underground networks, high-speed rail transport, aerospace and automobile industry, hospital management (including supplies and medical records), energy supply networks, etc., as well as in transversal areas that affect all of them, such as security and privacy.
This master degree will accept graduates in Computer Science Engineering, Software Engineering, Computer Engineering, Information Technology, and Information Systems with a strong interest in the mathematical rigor, reliability, and formalization of computer science problems, as well as graduates from equivalent degrees and from joint degrees with Informatics and Mathematics. Applications are also welcome from graduates in Technical Engineering for Computer Management, Computer Systems or other science or technology graduates, with appropriate supplementary training.
The working language of this master’s program is English. Spanish may be scarcely used in some elective courses. International graduates with an adequate command of English is therefore welcome to apply.
The increasing reliance on software systems of most industry sectors make it necessary to ensure that software is both absolutely reliable and resistant to external attacks. This has substantially increased the scope for employment in these sectors to include engineers with training in software development with rigorous methods. As a result, there is an evident increase in the use of formal techniques by software companies such as Microsoft, Facebook, Google, and Amazon, which needs to ensure that the software and services they provide are highly reliable. Added to this is the increasing relevance of rigorous verification of critical software in areas such as defense, and in the implementation of autonomous systems (personal assistants, self-driving vehicles) capable of decision making which needs to be tested or verified against their specifications.
This implies an ongoing demand for professionals who understand the techniques and tools developed in the field of formal methods and know-how to apply them to solve highly complex real-life problems where absolute accuracy must be guaranteed. Researching in academia or in research centers is of course another possible career path. Opportunities in the Madrid region include all of the Universities in Madrid, the IMDEA Software Institute, the IMDEA Networks Institute, and some Institutes in the CSIC. Universities and research centers in other areas of Spain, such as CERCA and ICREA in Cataluña, or CIC and BERC in the Basque Country, also consider computer science engineering as a priority research area and undertake research in fields where the computer science plays an essential role.
The master’s program consists of 60 credits: the compulsory core module Fundamental Formal Methods, with 3 courses (18 ECTS), and the elective module Complementary Formal Methods, with 5 courses (30 ECTS) chosen from the 10 available, one of which includes placements in companies or research groups. The program is completed with a supervisor-led master’s thesis (12 ECTS).