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.

COMPETENCIAS GENERALES

CG1 - Capacidad para proyectar, calcular y diseñar productos, procesos e instalaciones en todos los ámbitos de la Ingeniería Informática.

CG4 - Capacidad para la dirección general, dirección técnica y dirección de proyectos de investigación, desarrollo e innovación, en empresas y centros tecnológicos, en el ámbito de la Ingeniería Informática.

CG5 - Capacidad para la aplicación de los conocimientos adquiridos para resolver problemas en entornos nuevos o poco conocidos dentro de contextos amplios y multidisciplinares, siendo capaces de integrar dichos conocimientos.

CG7 - Capacidad para comprender trabajos de investigación y para crear nuevo conocimiento en el área de los métodos formalesaplicados a la Ingeniería Informática.

COMPETENCIAS TRANSVERSALES

CT1 - Capacidad para trabajar en equipo, ya sea como un miembro más o realizando la labor de dirección del mismo, promoviendoel libre intercambio de ideas.

CT2 - Capacidad para fomentar la creatividad tanto propia como la de los restantes miembros del equipo.

CT3 - Capacidad de razonamiento crítico como vía para mejorar la generación y desarrollo de ideas en un contexto profesional o deinvestigación.

CT4 - Capacidad para la búsqueda, análisis y síntesis de información.

CT5 - Capacidad para dirigir, planificar y surpervisar equipos multidisciplinares.

COMPETENCIAS ESPECÍFICAS

CE1 - Capacidad para expresar los requisitos y propiedades que ha de satisfacer un sistema informático, en una variedad delenguajes formales y a diferentes niveles de detalle.

CE2 - Capacidad para utilizar de forma competente las herramientas existentes de demostración automática y asistida de teoremas yde propiedades matemáticas.

CE3 - Capacidad para utilizar técnicas y herramientas avanzadas, automáticas y asistidas, para verificar formalmente que unprograma o sistema informático satisface las propiedades lógicas previamente especificadas.

CE4 - Capacidad para utilizar y desarrollar herramientas que analizan automáticamente propiedades de los programas, utilizandotan solo el texto fuente de los mismos.

CE5 - Capacidad para utilizar y desarrollar herramientas que analizan propiedades de los programas, mediante su ejecución en unconjunto de casos cuidadosamente seleccionado.

CE6 - Capacidad para utilizar modelos de cómputo alternativos a los convencionales, tales como la computación cuántica, los sistemas de reescritura, las máquinas abstractas, la programación con restricciones o los algoritmos bio-inspirados.

CE7 - Capacidad para aplicar técnicas matemáticas a problemas informáticos relevantes, tales como el diseño de protocoloscriptográficos seguros, la construcción de modelos formales del software, o el diseño de sistemas que aprenden automáticamentedurante su ejecución.

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.