Defensa Tesis Licenciatura Bruno Cuervo Parrino

• Título: Análisis de dataflow para mejorar la verificación de programas basada en SAT.
• Directores: Dr. Juan Pablo Galeotti y Dr. Diego Garbervetsky.
• Jurados: Lic. Esteban Pavese y Dr. Carlos Lopez Pombo.
• Resumen:

La verificación acotada de software basada en SAT consiste en la traducción del programa a analizar, junto con las anotaciones provistas por el usuario, a una fórmula proposicional. Posteriormente, la fórmula obtenida es analizada en busca de violaciones a la especificación usando un SAT-solver. Esta técnica es capaz de probar la ausencia de errores hasta un scope dado.

SAT es un problema NP-completo, lo que implica que no se conoce un algoritmo que lo resuelva eficientemente, siendo su complejidad exponencial en la cantidad de variables proposicionales. Es por esto que es esperable que una representación lógica de programa que apunte a reducir el número de variables tenga un gran impacto en la performance y escalabilidad del análisis.

TACO es una herramienta que implementa la traducción de Java con anotaciones JML a Alloy, un lenguaje formal relacional que permite analizar automáticamente especificaciones buscando contraejemplos de aserciones con la ayuda de un SAT-solver. TACO introduce una técnica para computar cotas más ajustadas para las variables en el estado inicial del programa.

En esta tesis mostramos cómo las técnicas de dataflow, típicamente utilizadas en la optimización de compiladores, pueden también ser usadas como un medio para obtener traducciones optimizadas. En particular, definimos e implementamos un análisis de dataflow que, utilizando las cotas iniciales provistas por TACO, computa el conjunto de valores que pueden ser asignados a variables locales y de instancia en cada punto del programa. Esta información es utilizada para eliminar variables innecesarias en la fórmula proposicional resultante de la traducción del programa.

Nuestros experimentos muestran mejoras significativas en los tiempos de análisis, permitiendo en algunos casos tanto la verificación de pruebas que no podían ser analizadas anteriormente como la extensión del scope del análisis.