Temas Subtemas
Bloque I: Validación de software
 I.1 Especificación, deseño e execución de probas
I1.1. Niveis e tipos de probas
I1.2. Propiedades e trazabilidade de requirimentos
I1.3. Automatización
I.2 Xestión de probas: planificación, avaliación, métricas e revisións
Bloque II: Métodos formais e razonamento automático
 II.1 Introdución: Dedución natural e cálculo de secuentes
II.2 Proba automática utilizando PVS
II.3 Que é e para que se utiliza un probador de teoremas?
II.4 Linguaxe de especificación de PVS: Tipos, expresións, teorías, subtipado
II.5 Probador PVS: tácticas, recursión, razoamento ecuacional
Bloque III: Comprobación por modelos (model checking) III.1 Introdución ás lóxicas modais temporais
III.2 Especificación de propiedades: deadlocks, safety, liveness, fairness
III.3 Funcionamento dun comprobador por modelos
III.4 Introdución ao manexo dunha ferramenta de model checking