La creación del software se enfrenta actualmente a grandes desafíos derivados del papel omnipresente del mismo en la sociedad actual: dependemos de programas que controlan dispositivos, vehículos, transacciones bancarias, el mercado de valores, aparatos médicos, etc. Aparte de los casos de pérdida de vidas humanas por fallos en el software, estos causan con frecuencia enormes trastornos en las vidas de millones de personas.  Hoy por hoy, el único método conocido para asegurar la corrección del software pasa por utilizar los llamados métodos formales, que se caracterizan a grandes rasgos por la modelización matemática del software, y de los procesos que este realiza, para conseguir demostrar que se cumplen los requisitos deseados.

Esta dependencia de la sociedad actual del software y la complejidad del mismo han hecho que este enfoque está recibiendo atención renovada en los últimos tiempos. Por ejemplo, Amazon usa bases distribuidas por todo el planeta que realizan millones de transacciones por segundo que deben ser coherentes, para lo cual se emplean algoritmos distribuidos extremadamente complejos. Los métodos tradicionales de desarrollo y testing no son capaces de encontrar errores sutiles en ellos, que causarían la pérdida de datos y el consiguiente perjuicio económico. Estos errores solo se manifiestan en una pequeña fracción de los posibles estados. Pero, dada la magnitud del software, sucederían con preocupante frecuencia de no encontrarse y resolverse, lo cual Amazon hizo mediante el uso de técnicas de verificación formal. Otro ejemplo revelador es el desarrollo del software de control de la línea 14 de metro de Paris, realizada íntegramente mediante métodos formales. Tras la generación del código, las pruebas durante la simulación y las realizadas en el entorno real no revelaron ningún error en las más de 80.000 líneasde código generadas automáticamente.

Por todo ello, también el entorno académico está ofreciendo másteres similares a este: Existen en las universidades de Oxford¹, en la École Polytehcnique Fedérale de Lausanne², en el University College of London³, o el Master Interuniversitario Parisino en Investigación en Informática⁴.

La formación adquirida en este máster conferirá una especial capacidad para aplicar métodos matemáticos a la resolución rigurosa de problemas informáticos. Consta de 60 créditos y ofrece al estudiante una amplia optatividad, pues estos han de elegir 30 créditos entre una oferta de 60. El Máster en Métodos Formales en Ingeniería Informática está encuadrado en el programa de posgrado de la Facultad de Informática, cuyo doctorado tiene concedida la "Mención de calidad" por la Agencia Nacional de Evaluación de la Calidad y Acreditación desde el año 2004, y la "Mención hacia la Excelencia" desde 2011. Estas menciones de calidad constituyen el máximo reconocimiento existente en España a la solvencia científico-técnica y formadora del programa de doctorado en su conjunto. 

El máster se impartirá preferentemente en inglés. Cuando se use el castellano, será siempre en asignaturas optativas. Por tanto, el máster se oferta también a estudiantes extranjeros que se desenvuelvan con solvencia en inglés.