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é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.