RT Dissertation/Thesis T1 Análisis de terminación de programas con controles de flujo complejos T2 Termination analysis of programs with complex control-flow A1 Doménech Arellano, Jesús Javier AB 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... AB 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... PB Universidad Complutense de Madrid YR 2021 FD 2021-05-28 LK https://hdl.handle.net/20.500.14352/11645 UL https://hdl.handle.net/20.500.14352/11645 LA eng NO Tesis de la Universidad Complutense de Madrid, Facultad de Informática, leída el 22-01-2021 DS Docta Complutense RD 9 abr 2025