Análisis de recursos de programas enteros y abstractosResource analysis of integer and abstract programs

Resumen

La inclusión de procesos informáticos en la vida cotidiana no puede ir ligada solo a la generación de componentes informáticos, sino también a su análisis y verificación. En concreto, el análisis de software se enfoca hacia el análisis del comportamiento de los programas informáticos para abordar propiedades como la seguridad, la corrección o la optimalidad. Además, la verificación y certificación del software durante el proceso de análisis ayuda a generar programas que cumplan de manera eficiente los requisitos exigidos. La primera parte de esta tesis está dedicada a una generalización del análisis automático de recursos en el ámbito de los programas abstractos, programas que contienen s¿¿mbolos o marcadores para representar instrucciones o expresiones sin especificar. Estos s¿¿mbolos aparecen habitualmente en reglas de transformación de programas. La técnica usada generaliza el análisis automático de recursos a un marco en el cual se manejan programas abstractos para, de esta manera, poder realizar un análisis del efecto de las transformaciones aplicadas a los programas. Este tipo de análisis se basa en componentes complejos que a menudo son externos al análisis de coste, por lo que, además de realizar este análisis de recursos, se añade al proceso de análisis la verificación y certificación de los resultados. De esta manera, la precisión de las cotas es comprobada antes de generar los resultados finales del análisis, generando además pruebas formales que pueden ser usadas en una etapa de certificación de los resultados. El análisis de recursos utilizado en la primera parte está basado en la inferencia de cotas superiores sobre el coste peor de los programas, ámbito al que se han dedicado la mayor¿¿a de los análisis de coste. Sin embargo, hay otras dos cotas importantes en el contexto del análisis de recursos: las cotas inferiores en el caso mejor y las cotas inferiores en el caso peor. Sobre las cotas inferiores en el caso peor versa la segunda parte de esta tesis, en la cual se desarrolla un nuevo método para sintetizar cotas inferiores en el caso peor de bucles enteros no deterministas. Esta técnica está basada en la búsqueda de una función que acota por debajo el número de iteraciones que realiza un bucle en el caso peor. La novedad más importante de esta técnica respecto a las anteriores es la inclusión de especialización de los bucles mediante la adición de restricciones a las posibles ejecuciones, buscando así encontrar cotas inferiores más precisas. La efectividad de esta técnica ha sido comprobada en un amplio conjunto de ejemplos, donde los resultados obtenidos han sido comparados con el sistema LoAT [1,2], sistema de referencia en la obtención de cotas inferiores en el caso peor. La unificación del análisis de programas abstractos con la s¿¿ntesis de cotas inferiores culmina los contenidos aportados por esta tesis en su última parte. La combinación de ambas cotas nos da una información más ajustada sobre el coste exacto que puede tener el programa. El cuarto capítulo de la tesis combina el análisis de coste de cotas inferiores y superiores con la verificación y certificación de los resultados obtenidos. El proceso de verificación da, de nuevo, la información necesaria para obtener cotas e invariantes suficientemente precisos para la certificación de los resultados. Dentro del marco de esta tesis, los resultados más importantes perseguidos han sido: - Estudio de la inclusión del análisis de recursos en el contexto de programas abstractos. - Desarrollo de un análisis de cotas inferiores del coste en el caso peor. - Unificación del análisis de coste de programas abstractos y de la inferencia de cotas inferiores. Referencias: [1] Florian Frohn et al. Inferring lower runtime bounds for integer programs. ACM Transactions on Programming Languages and Systems, 2020. [2] Florian Frohn et al. Lower runtime bounds for integer programs. In Automated Reasoning, 2016.