Isabel García gana el premio SISTEDES a la mejor tesis doctoral

La ex estudiante de doctorado del Instituto IMDEA Software, Isabel García-Contreras, gana uno de los dos premios a la mejor tesis de SISTEDES (Sociedad de Ingeniería de Software y Tecnologías de Desarrollo de Software). Se trata del segundo reconocimiento que recibe tras ser galardonada con el premio a la mejor tesis doctoral de la UPM para el curso 2020/2021.

“A scalable static analysis framework for reliable program development exploiting incrementality and modularity” es el título de su tesis, que fue dirigida por los profesores Manuel Hermenegildo y José Francisco Morales, ambos investigadores de IMDEA Software y profesores de la Escuela Técnica Superior de Ingeniería Informática de la Universidad Politécnica de Madrid.

Su objeto de estudio viene a responder a la fuerte tendencia de que el análisis y la verificación automáticos del código fuente son de gran importancia tanto a nivel de desarrollo como de mantenimiento de software.

La creciente importancia de la fiabilidad de un software en constante evolución se ha puesto de manifiesto por el número de herramientas y plataformas disponibles on-line para la integración y despliegue continuos de software. En este contexto, en el que los cambios ocurren rápido, las herramientas de análisis son  útiles sólo si son precisas y lo suficientemente escalables como para proporcionar resultados más rápidamente de lo que ocurren los cambios.

En esta tesis presenta diferentes algoritmos para reanalizar incrementalmente programas enteros, de forma sensible al contexto, reutilizando lo máximo posible un resultado anterior. Un aspecto novedoso y clave de su enfoque es aprovechar la estructura modular de los programas, típicamente definida por el programador, pero manteniendo una relación precisa entre el programa original y el resultado del análisis. Cabe destacar que todos los algoritmos han sido implementados y evaluados para diferentes dominios abstractos dentro de la herramienta CiaoPP.

Adicionalmente, presenta un mecanismo para que el programador pueda ayudar al analizador en términos de precisión y rendimiento mediante aserciones. Isabel muestra que estas aserciones, junto con un análisis incremental, son especialmente útiles para analizar código genérico.