Tema Subtema
Bloque I: Validación de software
 I.1 Especificación, diseño y ejecución de pruebas
I1.1. Niveles y tipos de pruebas
I1.2. Propiedades y trazabilidad de requisitos
I.2 Gestión de pruebas: planificación, evaluación, métricas y revisiones
Bloque II: Métodos formales y razonamiento automático
 II.1 Introducción: Deducción natural y cálculo de secuentes
II.2 Prueba automática utilizando PVS
II.3 ¿Qué és y para que se utiliza un probador de teoremas?
II.4 Lenguaje de especificación de PVS: Tipos, expresiones, teorías, subtipado
II.5 Probador PVS: tácticas, recursión, razonamiento ecuacional
Bloque III: Comprobación por modelos (model checking) III.1 Introducción a las lógicas modales temporales
III.2 Especificación de propiedades: deadlocks, safety, liveness, fairness
III.3 Funcionamiento de un comprobador por modelos
III.4 Introducción al manejo de una herramienta de model checking