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

dc.contributor.advisorBarthe, Gilles
dc.contributor.advisorKunz, César
dc.contributor.authorSamborski-Forlese, Julián
dc.date.accessioned2013-03-25T19:48:47Z
dc.date.available2013-03-25T19:48:47Z
dc.date.issued2009-05-12
dc.description.abstractLa 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.es
dc.description.affiliationFil: Samborski-Forlese, Julián. Tesista del Departamento de Ciencias de la Computación. Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario; Argentina.
dc.description.peerreviewedPeer reviewedes
dc.identifier.urihttp://hdl.handle.net/2133/2331
dc.language.isospaes
dc.publisherFacultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosarioes
dc.relation.publisherversionhttp://www.fceia.unr.edu.ar/lcc/t523/tesina.php?campo1=17es
dc.rightsopenAccesses
dc.subjectProducción de softwarees
dc.subjectMétodos Híbridos de verificaciónes
dc.titlePreservación de Obligaciones de Prueba en Entornos Híbridos de Verificación
dc.typebachelorThesis
dc.typetesis de grado
dc.typepublishedVersion

Archivos

Bloque original
Mostrando 1 - 1 de 1
Cargando...
Miniatura
Nombre:
17.pdf
Tamaño:
500.55 KB
Formato:
Adobe Portable Document Format
Bloque de licencias
Mostrando 1 - 1 de 1
Nombre:
license.txt
Tamaño:
2.95 KB
Formato:
Item-specific license agreed upon to submission
Descripción: