Máster Universitario en Software y Sistemas

Interpretación Abstracta

Profesor (Coordinador):
Manuel Carro
mcarro@fi.upm.es
Profesor:
Pierre Ganty
pierre.ganty@imdea.org

Semestre

Segundo semestre

Créditos

4 ECTS

Resumen

La interpretación abstracta es un marco matemático formal que permite definir e implementar análisis de programas que son correctos por construcción - siempre que se cumplan algunas propiedades básicas. El software es una parte esencial de sistemas cada vez más complejos. Para dominar esa complejidad, es necesario calcular automáticamente información confiable sobre el software. Este es el objetivo del análisis estático. Para razonar rigurosamente sobre los programas, se desarrollan modelos matemáticos de comportamiento o programas. Estos modelos se denominan semánticas. Dependiendo de las propiedades a calcular, podemos usar semánticas diferentes - algunas más detalladas para más precisión, otros menos para una mayor eficiencia. La interpretación abstracta es una teoría de la aproximación que permite la comparación de semánticas diferentes, o la construcción de nuevas semánticas a través del refinamiento o la abstracción. Dado que todas las propiedades interesantes de los programas son indecidibles, todos los métodos de análisis estático introducen aproximaciones de una u otra manera. Por lo tanto, la interpretación abstracta es un buen marco para dar una visión unificada de tales métodos y para compararlos.

Objetivos

Programa

  1. Una introducción informal
  2. Propiedades del programa
  3. Aproximaciones de la propiedad
  4. Morfismos y conexiones
  5. Abstracción de puntos fijos
  6. Concepción del análisis de alcanzabilidad
  7. Aplicaciones
  8. Puntos fijos aproximados y ensanchamiento
  9. Refinamiento de los análisis

Web de la Asignatura

http://www.software.imdea.org/graduateschool

Prerrequisitos

Método de Evaluación

Idioma en que se imparte

Inglés

Competencias Específicas

Más información:

Esta tabla muestra el código, la descripción y el nivel de cada una de las competencias específicas de la asignatura

Código Competencia Nivel
CEM1 Identificar, a partir del estado de la cuestión, la presencia de problemas de investigación relacionados con la concepción, la construcción, el uso y la evaluación de sistemas sociotécnicos complejos que hagan un uso intensivo de software. S
CEM5 Aportar soluciones a aquellos problemas abiertos relacionados con el ámbito de aplicación y los métodos, técnicas y herramientas de Verificación y Validación de Software. A

Resultados de Aprendizaje

Más información:

Esta tabla muestra cada el código, la descripción, las competencias asociadas y el nivel de adquisición de cada uno de los resultados de aprendizaje de la asignatura

Código Resultado de Aprendizaje Competencias asociadas Nivel de Adquisición
RA-AV-8 Ser capaz de utilizar las herramientas existentes para el Análisis estático de programas, la Verificación formal de programas y la Transformación automática de programas CEM5 A
RA-AV-9 Conocer los fundamentos de la interpretación abstracta como método de análisis estático de programas. CEM1 C

Guía de Aprendizaje

Guía de aprendizaje de la asignatura: Interpretación Abstracta