La tesis estudia la verificación formal de propiedades temporales de safety y liveness en sistemas concurrentes parametrizados, enfocándose principalmente en programas que manipulan complejas estructuras de datos concurrentes en la memoria dinámica. Este trabajo presenta un marco formal basado en métodos deductivos que, de manera clara, permite separar el razonamiento entre el control del flujo del programa y los tipos de datos que se manipulan. El control del flujo es analizado utilizando novedosas técnicas deductivas de verificación especialmente designadas para lidiar con sistemas parametrizados. Comenzando a partir de un programa concurrente y la especificación de una propiedad temporal, las técnicas deductivas propuestas son capaces de generar un conjunto finito de condiciones de verificación cuya validez implican la satisfacción de dicha especificación temporal por parte de cualquier sistema, sin importar el número de procesos que formen parte del sistema. Al mismo tiempo, la tesis explora la construcción de teorías decidibles y procedimientos de decisión sobre estructuras de datos complejas que son capaces de verificar de manera automática las condiciones de verificación que hayan sido generadas anteriormente. Finalmente, el marco formal completo es evaluado probando propiedades de safety y liveness sobre un conjunto de programas que incluyen protocolos de exclusión mutua y estructuras de datos basadas en punteros.
Alejandro Sánchez ha sido supervisado por César Sánchez, investigador de Instituto IMDEA Software y ha obtenido su grado de doctor de la Universidad Politécnica de Madrid con mención “cum laude”.
