Avances recientes en análisis estáticos de terminación

Abstract

En los últimos años han aparecido un número bastante considerable de trabajos sobre análisis de terminación de programas que han supuesto la base teórica de una serie de herramientas prácticas que han dado lugar a resultados bastante prometedores. Nos proponemos presentar algunas de las técnicas más recientes de detección de terminación de programas entre las que hemos destacado la técnica Size-Change Termination (SCT) propuesta por Ben-Amram, Lee y Jones [POPL’ 01] con algunas de sus variantes, y otras técnicas basadas en metodos lineales como la propuesta por Podelski y Rybalchenko [VMCAI’ 04] que tienen por objeto inferir funciones de rango para probar la terminación de los programas. Como resultado de nuestro trabajo hemos implementado algunas de estas técnicas con el objetivo de llevarlas a la práctica en el lenguaje funcional de primer orden Safe. [Abstract] In recent years, they have published a fairly large number of works about program termination analysis that have provided the theoretical basis of some practical tools leading to some promising results. We present some of the latest techniques for detecting program termination. We have highlighted the Size-Change Termination (SCT) framework proposed by Ben-Amram, Lee and Jones [POPL’ 01] with some of its variants, and other techniques based on linear methods as proposed by Podelski and Rybalchenko [VMCAI’ 04] whose aim is to infer ranking functions to prove program termination. As a result of our work, we have implemented some of these methods in order to apply them in the first-order functional language Safe.