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

DSpace/Manakin Repository

Show simple item record

dc.contributor.advisor Barthe, Gilles
dc.contributor.advisor Kunz, César
dc.contributor.author Samborski-Forlese, Julián
dc.date.accessioned 2013-03-25T19:48:47Z
dc.date.available 2013-03-25T19:48:47Z
dc.date.issued 2009-05-12
dc.identifier.uri http://hdl.handle.net/2133/2331
dc.description.abstract 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. es
dc.language.iso spa es
dc.publisher Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario es
dc.rights openAccess es
dc.subject Producción de software es
dc.subject Métodos Híbridos de verificación es
dc.title Preservación de Obligaciones de Prueba en Entornos Híbridos de Verificación
dc.type bachelorThesis
dc.type tesis de grado
dc.type publishedVersion
dc.description.peerreviewed Peer reviewed es
dc.relation.publisherversion http://www.fceia.unr.edu.ar/lcc/t523/tesina.php?campo1=17 es
dc.description.affiliation Fil: 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.


Files in this item

This item appears in the following Collection(s)

Show simple item record

My Account


Search DSpace


Browse

Statistics