Análisis de terminación de programas con controles de flujo complejos

Abstract

El problema de la terminación de un programa es fundamental en la informática y ha sido objeto de estudio de numerosas investigaciones. La técnica mejor conocida, y más frecuentemente utilizada, para demostrar terminación es la del uso de funciones de clasificación (ranking functions). Estas funciones relacionan los estados del programa con los elementos de un conjunto ordenado bien-fundado, tal que el valor desciende en estado consecutivos del programa. Como descender en un conjunto ordenado bien-fundado no se puede hacer de manera infinita se demuestra la terminación del programa. Es esta tesis, abordamos el problema de terminación para Sistemas de Transiciones (Transition Systems) con valores numéricos, que son una representación de programas muy comúnmente utilizada en los análisis de programas. Los Sistemas de Transiciones están definidos por Grafos de Control de Flujo (Control-Flow Graph) donde las aristas están anotadas con fórmulas describiendo las transiciones que hay entre los nodos correspondientes...The problem of the program termination is fundamental in Computer Science and has been the subject of voluminous research. The best known, and often used technique for proving termination is that of ranking functions. These are functions that map the program states to the elements of a well-founded ordered set, such that the value descends on consecutive program states. Since descent in a well-founded set cannot be infinite, this proves terminatio. In this thesis, we address the termination problem for Transition Systems with numerical variables, which is a very common program representation that is often used in program analysis. They are defined by Control-Flow Graphs where edges are annotated with formulas describing transitions between corresponding nodes...