Preservación de Obligaciones de Prueba en Entornos Híbridos de Verificación

La producción de software confiable y eficiente requiere, al menos en parte, la automatización de su construcción. Para alcanzar este objetivo es indispensable estudiar a los programas y sus ejecuciones como objetos matemáticos. Los entornos de verificación de programas se basan cada vez más en méto...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Samborski-Forlese, Julián
Otros Autores: Barthe, Gilles
Formato: bachelorThesis tesis de grado publishedVersion
Lenguaje:Español
Publicado: Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario 2013
Materias:
Producción de software
Métodos Híbridos de verificación
Acceso en línea:http://hdl.handle.net/2133/2331
http://hdl.handle.net/2133/2331
Aporte de:
Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR) de Universidad Nacional de Rosario
id I15-R121-2133-2331
record_format dspace
institution Universidad Nacional de Rosario
institution_str I-15
repository_str R-121
collection Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR)
language Español
orig_language_str_mv spa
topic Producción de software
Métodos Híbridos de verificación
spellingShingle Producción de software
Métodos Híbridos de verificación
Samborski-Forlese, Julián
Preservación de Obligaciones de Prueba en Entornos Híbridos de Verificación
topic_facet Producción de software
Métodos Híbridos de verificación
description La producción de software confiable y eficiente requiere, al menos en parte, la automatización de su construcción. Para alcanzar este objetivo es indispensable estudiar a los programas y sus ejecuciones como objetos matemáticos. Los entornos de verificación de programas se basan cada vez más en métodos híbridos que combinan análisis estático con generación de condiciones de verificación. Mientras que dichos entornos de verificación operan sobre programas fuente, a menudo es preferible obtener garantías sobre código ejecutable. El objetivo de este trabajo es mostrar que, para métodos híbridos de verificación basados en análisis estático y generación de condiciones de verificación, la compilación de programas preserva obligaciones de prueba y, en consecuencia, es posible transferir evidencia de ciertas propiedades de programas fuente a programas compilados. Este resultado se sustenta en la preservación de soluciones de análisis por compilación. Esto se logra apoyándose en un análisis de bytecode que realiza una ejecución simbólica de las expresiones del stack con el fin de evitar la pérdida de precisión que conlleva realizar análisis estático en código compilado. Se muestra, además, que los métodos híbridos de verificación son correctos, probando que todo programa demostrable por dichos métodos es también demostrable (a un costo mayor) por métodos estándares. Finalmente, se presenta un caso de estudio en el que se analizan algunas de las principales ventajas que brindan los métodos híbridos en comparación con los métodos clásicos.
author2 Barthe, Gilles
author_facet Barthe, Gilles
Samborski-Forlese, Julián
format bachelorThesis
tesis de grado
publishedVersion
author Samborski-Forlese, Julián
author_sort Samborski-Forlese, Julián
title Preservación de Obligaciones de Prueba en Entornos Híbridos de Verificación
title_short Preservación de Obligaciones de Prueba en Entornos Híbridos de Verificación
title_full Preservación de Obligaciones de Prueba en Entornos Híbridos de Verificación
title_fullStr Preservación de Obligaciones de Prueba en Entornos Híbridos de Verificación
title_full_unstemmed Preservación de Obligaciones de Prueba en Entornos Híbridos de Verificación
title_sort preservación de obligaciones de prueba en entornos híbridos de verificación
publisher Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario
publishDate 2013
url http://hdl.handle.net/2133/2331
http://hdl.handle.net/2133/2331
work_keys_str_mv AT samborskiforlesejulian preservaciondeobligacionesdepruebaenentornoshibridosdeverificacion
bdutipo_str Repositorios
_version_ 1764820411950825474

Ejemplares similares