La formación adquirida en el máster conferirá capacidad para aplicar métodos matemáticos a la resolución rigurosa de problemas informáticos. El objetivo es formar profesionales altamente cualificados que puedan enfrentarse con éxito al diseño fiable de sistemas que no toleren errores, a su correcto despliegue, y a la evaluación o auditoría de sistemas de terceros. También persigue proporcionar una formación básica a futuros investigadores en el área de los métodos formales.

La mayor parte de los errores que aparecen en los sistemas informáticas tienen su raíz en una formalización pobre, o inexistente, de los requisitos, de su diseño, y de la ausencia de verificación rigurosa de su implementación. Este máster mejorará la capacidad de los egresados para evitar tales errores y para realizar diseños de sistemas y programas más limpios, resistentes, y comprensibles, así como la verificación de los mismos. Serán, por tanto, profesionales muy cualificados que podrán abordar problemas informáticos muy complejos en los que sea necesaria una alta fiabilidad. Estos problemas aparecen en empresas de alta tecnología, como las que desarrollan o mantienen productos en las áreas de las telecomunicaciones, el transporte aéreo, las redes de metro, el transporte ferroviario de alta velocidad, la industria aeroespacial y automovilística, la gestión de material hospitalario, las redes de distribución de energía, y otras similares, así como en áreas transversales a todas ellas, tales como la seguridad y la privacidad.

Las potenciales vías de inserción laboral se incrementan de forma sustancial debido a la imparable informatización de las industrias mencionadas en el apartado de objetivos y a la necesidad de que el software que utilizan sea absolutamente fiable, y a la vez resistente aataques externos. Cabe destacar el uso creciente de técnicas formales por algunas de las grandes empresas de software, o proveedores de servicios, tales como Microsoft, Facebook, Google, o Amazon, que deben asegurar que el software y servicios que proporcionan para un uso masivo sea altamente fiable, así como la creciente relevancia de las pruebas rigurosas de corrección de software crítico en los ámbitos de defensa y en la implementación de sistemas autónomos (asistentes personales, automóviles que conducen solos), capaces de tomar decisiones que se puedan probar acertadas con respecto a una especificación. Cada vez serán más necesarios, por tanto, profesionales que conozcan las técnicas y herramientas desarrolladas en el ámbito de los métodos formales, y que sepan aplicarlas a la resolución de problemas reales de gran complejidad, o que requieran garantías absolutas de corrección.

Otra vía de inserción es la de continuar con una carrera investigadora endepartamentos universitarios y centros de investigación. En la Comunidad de Madrid, podemos contar entre ellos el Instituto IMDEA Software, el Instituto IMDEANetworks y algunos institutos del CSIC. Por supuesto, también en universidades ycentros de investigación de otras comunidades, como los de la red CERCA y el ICREA en Cataluña, o los centros CIC y BERC en el País Vasco, parte de Ikerbasque, que o bien tienen a la Ingeniería Informática como área de investigación primordial, o bien investigan en áreas en las quela informática juega un papel esencial.