2026-07-20T01:04:42Zhttps://docta.ucm.es/rest/oai/requestoai:docta.ucm.es:20.500.14352/660842023-07-19T05:16:21Zcom_20.500.14352_1col_20.500.14352_8
Docta Complutense
advisor
Peña Mari, Ricardo Vicente
author
Holubanský, Jakub
author
Mínguez Horcajada, Álvaro
2023-06-21T06:19:18Z
2023-06-21T06:19:18Z
2016
https://hdl.handle.net/20.500.14352/66084
De entre una serie de métodos estudiados acerca de la terminación de algoritmos, tales como Size-Change Termination o Isabelle, elegimos el método de RANK como instrumento para desarrollar nuestro propio programa de detección de terminación sobre el lenguaje de la IR. Esta decisión se basa en el coste polinómico de este método (frente a costes en PSPACE como el Size-Change Termination)y la posibilidad de obtener una herramienta asociada al mismo que además nos da la posibilidad de conocer un tiempo de ejecución aproximado.
La herramienta asociada a RANK es compleja y va de la mano de una segunda herramienta (ASPIC). Hemos estudiado varios ejemplos, tales como el Mergesort o el Quicksort, para explicar la utilización de estas dos herramientas y a su vez ponernos en situación de los diferentes problemas que nos podemos encontrar a la hora de estudiar un programa.
Partiendo del proceso que hemos usado para construir los automátas de los ejemplos anteriores, hemos diseñado e implementado en Java un algoritmo para transformar programas en el lenguaje de la IR al formato de entrada de RANK. Los resultados han sido satisfactorios, puesto que con los autómatas generados somos capaces de detectar de forma automatizada la terminación de, entre otros, los algoritmos recursivos antes mencionados.
spa
Atribución-NoComercial 3.0 España
Análisis de terminación para una plataforma de verificación de programas
bachelor thesis
URL
https://docta.ucm.es/bitstreams/68af5f82-5320-4cea-8666-d1514f846ebe/download
File
MD5
3b7b6b3b62fad3acdf9a02e82b450164
1776828
application/pdf
proyecto.pdf