Ir al contenido

Doctorado en Tecnologías para el Desarrollo de Sistemas Software Complejos

Análisis, Depuración y Optimización de Software

Profesor:
Álvaro Germán Puebla Sánchez
Despacho:
D-2301
Teléfono:
91 336 7453
e-mail:
german@fi.upm.es
Profesor:
James Lipton
e-mail:
jlipton@fi.upm.es
Créditos:
6
Concentración:
Principal
Cuatrimestre:
Segundo

Resumen:

Se presentan los fundamentos y las técnicas del análisis de programas, en particular la de la interpretación abstracta. Se pretende que el alumno se familiarice con el análisis y la depuración automáticos de programas basados en métodos formales. Se estudian sistemas formales para la especificación y depuración de programas y métodos de comprobación simbolica de modelos (Symbolic Model Checking) con el objetivo de que el alumno sea capaz de utilizar herramientas existentes para análisis y verificación de programas y comprobación simbólica de modelos. Por último, se estudian conceptos de código móvil, en especial en entornos Java, de seguridad del código móvil y de código con demostración (Proof-Carrying Code).

Objetivos:

Programa:

  1. Técnicas de análisis de programas.
  2. Interpretación abstracta.
  3. Sistemas formales para la especificación y depuración de Programas.
  4. Métodos de comprobación simbolica de modelos (Symbolic Model Checking).
  5. Código móvil: Java y código de byte de Java.
  6. Seguridad de código móvil.
  7. Código con demostración (Proof-Carrying Code).

Bibliografía:

Prerrequisitos:

Ninguno

Método de Evaluación:

Idiomas en que se imparte:

Inglés