Ir al contenido

Inicio
ETSIINF en Twitter ETSIINF en Facebook
Inicio > Estudios > Másteres oficiales > Métodos Formales en Ingeniería Informática

Máster Interuniversitario en

Métodos Formales en Ingeniería Informática

Por la UCM, la UPM y la UAM

Band

Motivación

Fechas Importantes

  • Preinscripción 2019: 1 febrero a 31 mayo
  • Publicación de listas admitidos 2019: 15 de marzo y 15 de junio
  • Fechas para entregar documentación:
    • De universidades españolas: 15 julio
    • De universidades extranjeras: 14 octubre

Consulta en cualquier caso la página oficial de la Universidad para tener la información más actualizada.

Si vienes de un país externo a la UE, recomendamos encarecidamente hacer la preinscripción lo antes posible para tener tiempo a realizar los trámites de obtención de visado.

Inscribete
 
Los sistemas informáticos actuales son omnipresentes y necesarios. Desde conducir un coche hasta hacer la compra de un libro o una llamada telefónica, casi todos nuestros actos cotidianos necesitan la intermediación del software --- por tanto dependemos de él y de su buen funcionamiento.  Por desgracia, con frecuencia se producen errores que afectan este buen funcionamiento.
La mayor parte de los errores graves en los sistemas informáticos actuales están causados por una formalización pobre de los requisitos o su diseño, o en la ausencia de una verificación rigurosa de su implementación.  Este Máster se centra en mostrar técnicas para evitar esos errores y realizar sistemas y programas más limpios, resistentes, comprensibles y mantenibles.
Este Máster se dirige a informáticos con vocación por el rigor y la fiabilidad de los sistemas informáticos.  El objetivo de esta titulación es formar profesionales que sean capaces de abordar problemas informáticos complejos como establecer la corrección del código, usando herramientas matemáticas rigurosas.  Estos profesionales podrán enfrentarse con éxito al diseño de software fiable, a su correcto despliegue y a la evaluación y verificación de software de terceros.  Este Máster también se propone formar futuros investigadores en el área de los métodos formales.
Su carácter Interuniversitario (UCM, UPM, UAM) permite la participación de profesores reconocidos pertenecientes a las tres Universidades, además de un intercambio de conocimientos entre los alumnos. 
 

 

 

Características

Dirigido a...

Si eres un graduado en Ingeniería Informática o en Matemáticas e Informática (bien de doble grado o de grado conjunto) y te ha atraído la programación y tienes pasión por asegurar que tu código funcione siempre sin fallos y por descubrir el algoritmo que resuelve ese problema de la manera más segura y óptima, entonces este puede ser tu máster. Buscamos estudiantes con vocación por la fiabilidad y que no rehuyan una formalización de los problemas y las herramientas. 

Aparte de los mencionados arriba, también pueden acceder al máster titulados en disciplinas afines (matemáticas, telecomunicaciones...) quizá cursando complementos formativos para asegurar una base inicial que les permita seguir los estudios.

Compañías futuro

 

Beneficios

El uso de métodos formales se ha incrementado notablemente en los últimos años, de la mano de la creciente complejidad de los sistemas informáticos.  Las grandes empresas de internet, los proveedores de redes sociales, los distribuidores de contenidos, los fabricantes de sistemas empotrados, las empresas de votación electrónica, entre otras muchas, necesitan código cuya corrección esté garantizada.

Por ello, tanto estas empresas como los fabricantes de software están poniendo un interés creciente en profesionales con conocimiento de métodos formales en todas sus variantes.  De manera similar, los centros de investigación y las universidades están ofreciendo de manera cada vez más generalizada la oportunidad de seguir una carrera investigadora centrada en el avance y la aplicación de los métodos formales.

 

 

Asignaturas

 

Primer semestre (septiembre-enero)

Asignatura Tipo ECTS Descripción
Análisis estático de programas y resolución de restricciones Obligatoria 6 El análisis estático de programas determina, sin necesidad de ejecutar un programa, qué propiedades tiene. Ayuda a asegurar que los programas hacen lo que se espera de ellos y a optimizarlos automáticamente.
Modelos de la concurrencia Obligatoria 6 En la mayor parte de las aplicaciones actuales hay interacciones entre hilos de ejecución.  Entender estos modelos de interacción ayuda a diseñar arquitecturas correctas desde el principio.
Teoría de lenguajes de programación Obligatoria 6 Los lenguajes de programación actuales tienen en común más de lo que parece. Comprender sus bases permite distinguir qué características son diferenciadoras y cuáles son accesorias.
Desarrollo formal de software dirigido por modelos Optativa 6 Usar lenguajes específicos para un dominio facilita la realización de software complejo.  El aplicar métodos formales a estas soluciones permite llegar a código ejecutable con las propiedades requeridas.
Diseño de algoritmos bioinspirados Optativa 6 Las soluciones encontradas por la naturaleza a determinados problemas pueden adoptarse y reproducirse en software para resolver problemas similares de forma eficiente.
Aprendizaje automático Optativa 6 Los últimos avances en aprendizaje automático permiten que los ordenadores lleven a cabo tareas sin solución algorítmica satisfactoria.  Conocer estas técnicas permite decidir la adecuación de soluciones basadas en AA.
Diseño y Análisis de Protocolos de Seguridad
Optativa 6 No disponible en este curso
Métodos formales de testing Optativa 6 Las pruebas con casos (testing) son  la forma más extendida de determinar si un programa se comporta como se espera.  El testing no da una certeza absoluta, pero su fiabilidad incrementarse notablemente si se complementa con un enfoque formal.

 

Segundo semestre (febrero-mayo)

Asignatura Tipo ECTS Descripción
Análisis de sistemas concurrentes y distribuidos Optativa 6 La descomposición en varios hilos de ejecución es una ubicua las aplicaciones de hoy en día  Su análisis tiene muchas características propias que hacen que deben estudiarse específicamente.
Diseño de sistemas correctos por construcción Optativa 6 El software puede construirse dividiéndolo en varias etapas bien definidas y probar que cada estado respeta las propiedades desadas y no viola las ya probadas para terminar con un sistema complejo que es correcto porque cada paso de su construcción lo es.
Computación cuántica Optativa 6 El incremento de la potencia de cálculo que traería la computación cuántica abre la posibilidad de resolver problemas inabordables hoy en día. Esta asignatura mostrará las bases y las aplicaciones de la computación cuántica.
Verificación asistida de programas Optativa 6 Verificar que un programa se comporta como se espera con involucra pruebas matemáticas a veces complejas y usualmente, tediosas  Usar herramientas automatizadas incrementa la productividad del ingeniero de software y la confianza en las pruebas.
Prácticas en empresas o grupos de investigación Optativa 6 Pueden reconocerse estancias en empresas e instituciones de investigación con créditos lectivos  Estas estancias son enriquecedoras y permiten aplicar y ampliar las técnicas aprendidas en las asignaturas.
Trabajo de fin de máster Obligatorio 12 El TFM puede ser dirigido por profesores del máster de cualquiera de las universidades participantes, independientemente de dónde se haya matriculado el alumno.

 

Horarios del curso 2018-2019 (seleccionar "MÁSTER MÉTODOS FORMALES")

 

Estancias en empresas e instituciones de investigación

El máster contempla la posibilidad de realizar hasta 6 ECTS como estancias en empresas de base tecnológica e instituciones de investigación.  En particular, el Instituto IMDEA Software es una de las Instituciones de la comunidad de Madrid que realiza investigación en temas cercanos a la temática del Máster y en la que se podrían realizar internships.

Profesorado

Todo el profesorado participante en el máster tiene actividad investigadora ininterrumpida en los últimos años y participa en o lidera proyectos de investigación.

Información adicional

Pasos para formalizar la matriculación en la UPM

La lista que sigue es un resumen de los pasos necesarios para realizar la matrícula de Máster en la UPM.  Consulta la web de la UPM para tener una información más completa - las necesidades son diferentes dependiendo de tu origen.  Toda la documentación debe estar en español o en inglés, bien porque sea así originalmente o mediante una traducción jurada.

  1. Realiza la preinscripción, para lo que es necesario proporcionar, escaneados:
  2. Esta documentación es examinada para comprobar que se cumplen los requisitos de longitud de los estudios, existencia de un título de grado, y comprobación de que los estudios proporcionan una base suficiente para continuar con el máster elegido.
  3. Publicación de listas de admitidos.  Las listas se actualizan periódicamente según se evalúan las solicitudes.
  4. En caso de estar admitido, recibirás por correo electrónico una carta de aceptación en el máster y tendrás una cuenta de alumno en la UPM.
  5. Si necesitas un visado porque vienes desde un país extranjero, necesitarás esa carta en el consulado español que te corresponda.
  6. Tras la admisión es necesario realizar la formalización de la matrícula, en la que se eligen las asignaturas que se quieren cursar.  Se puede hacer personalmente en la Escuela Técnica Superior de Ingenieros Informáticos (ETSIINF) o mediante la web.
  7. Solicitar personalmente en la ETSIINF la generación de una carta de pago para ingresar el coste de la matrícula. Tras ello, entrega el justificante del abono junto con los originales de los documentos que se hayan entregado a través de web en el primer paso de esta lista.

Contacto e información

Información en las demás universidades participantes

 

Band