Publication:
Análisis de terminación para una plataforma de verificación de programas

dc.contributor.advisorPeña Mari, Ricardo Vicente
dc.contributor.authorHolubanský, Jakub
dc.contributor.authorMínguez Horcajada, Álvaro
dc.date.accessioned2023-06-21T06:19:18Z
dc.date.available2023-06-21T06:19:18Z
dc.date.issued2016
dc.degree.titleGrado en Ingeniería Informática
dc.descriptionTrabajo de Fin de Grado en Ingeniería Informática (Universidad Complutense, Facultad de Informática, curso 2015/2016)
dc.description.abstractDe 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.
dc.description.departmentDepto. de Sistemas Informáticos y Computación
dc.description.facultyFac. de Informática
dc.description.refereedTRUE
dc.description.statusunpub
dc.eprint.idhttps://eprints.ucm.es/id/eprint/39842
dc.identifier.urihttps://hdl.handle.net/20.500.14352/66084
dc.language.isospa
dc.page.total53
dc.rightsAtribución-NoComercial 3.0 España
dc.rights.accessRightsopen access
dc.rights.urihttps://creativecommons.org/licenses/by-nc/3.0/es/
dc.subject.cdu004.421(043.3)
dc.subject.cdu519.852(043.3)
dc.subject.keywordAnálisis de terminación
dc.subject.keywordVerificación de programas
dc.subject.keywordProgramación líneal
dc.subject.keywordAutómatas finitos con variables enteras
dc.subject.keywordTermination analysis
dc.subject.keywordProgram verification
dc.subject.keywordLinear programming
dc.subject.keywordInteger interpreted automata
dc.subject.ucmProgramación de ordenadores (Informática)
dc.subject.ucmLógica simbólica y matemática (Matemáticas)
dc.subject.unesco1203.23 Lenguajes de Programación
dc.subject.unesco1102.14 Lógica Simbólica
dc.titleAnálisis de terminación para una plataforma de verificación de programas
dc.title.alternativeAnalysis termination for a program verification platform
dc.typebachelor thesis
dspace.entity.typePublication
Files
Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
proyecto.pdf
Size:
1.69 MB
Format:
Adobe Portable Document Format