Análisis y verificación de programas modulares

Resumen

Existe un gran número de técnicas avanzadas de verificación y optimización estática de programas que han demostrado ser extremadamente útiles en la detección de errores de programación y en la mejora de la eficiencia, y que tienen como factor común la necesidad de información precisa de análisis global del programa, La interpretación abstracta es una de las técnicas de análisis más establecidas, lo que ha permitido el desarrollo de métodos innovadores para la verificación de programas. Por otra parte, uno de los desafíos más importantes en la investigación informática actual consiste en mejorar la capacidad de detectar automáticamente errores en programas y asegurar que un programa es correcto respecto a una determinada especificación, con el objetivo de producir software. Por ello, la verificación de programas es un área importante de investigación, y por ello proporcionar técnicas avanzadas para detectar errores y verificar sistemas en programas reales complejos es una de las áreas más relevantes en la industria informática actual. Un enfoque interesante de la verificación de programas es la denominada verificación abstracta, una técnica que tiene como objetivo la verificación de un programa mediante sobre-aproximaciones de la semántica concreta del programa. Sin embargo, estos métodos no son directamente aplicables a programas reales, pues técnicas avanzadas como las mencionadas están en muchos casos disponibles como prototipos, y los avances conseguidos hasta ahora en esta dirección solamente han permitido su aplicación de modo restringido. El objetivo de esta Tesis Doctoral es desarrollar técnicas de análisis y verificación para su uso eficiente y preciso en grandes programas modulares o incompletos y mostrar su factibilidad en sistemas reales. Con el fin de evaluar la utilidad práctica de las técnicas propuestas, los algoritmos resultantes han sido implementados e integrados en el sistema Ciao y se han comprobado experimentalmente, lo que ha permitido aplicarlos en casos de estudio reales.