La investigadora del Instituto IMDEA Software presentó de manera exitosa su tesis el pasado miércoles 21 de julio. “A scalable static analysis framework for reliable program development exploiting incrementality and modularity” es el título del trabajo desarrollado por la investigadora, dirigido por el distinguido profesor y ex director del Instituto, Manuel Hermenegildo. Con esta tesis, Isabel finaliza sus estudios de doctorado en inteligencia artificial de la Universidad Politécnica de Madrid (UPM).
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.
Las herramientas automáticas de análisis estático permiten inferir propiedades del software sin ejecutarlo y sin necesidad de intervención humana. Si dichas herramientas se basan en métodos formales, éstas proporcionan garantías matemáticas de que las propiedades se cumplen. El uso de estas herramientas durante las fases de codificación, prueba y mantenimiento del ciclo de desarrollo del software ayuda a reducir esfuerzo en términos de tiempo y coste, ya que contribuye a la detección temprana de errores, a la optimización automática y a la documentación automática.
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.
Por último, presenta una aplicación de este marco de análisis para realizar comprobación de aserciones en tiempo de compilación al vuelo, de forma que se proporciona una retroalimentación continua al programador mientras escribe el código. Su experiencia inicial con esta herramienta integrada muestra resultados bastante prometedores, con tiempos de latencia bajos que proporcionan una retroalimentación semántica temprana, continua y precisa “sobre la marcha” a los programadores durante el proceso de desarrollo. Por tanto, la herramienta permite detectar muchos tipos de errores, como variables intercambiadas, incompatibilidades de propiedades, llamadas ilegales a predicados de la biblioteca, restricciones numéricas violadas, comportamientos no deseados con respecto a la terminación, uso de recursos, determinismo, la cobertura y el fracaso, etc.
