Análisis modular y recuperación de contraejemplos en TACO

Abstract

TACO es una herramienta para realizar verificación formal de programas, que permite detectar bugs en los mismos. Esta traduce un programa escrito en lenguaje Java y su especificación en JML a la notación DynAlloy, para luego analizar la especificación obtenida mediante SAT solving, vía una traducción adicional al lenguaje Alloy. En este trabajo presentamos dos mejoras significativas a esta herramienta y técnica de análisis. En primer lugar, proveemos un mecanismo de análisis modular de código en presencia de invocación de rutinas. En segundo lugar, automatizamos la construcción de unit tests en Java, que reproducen los bugs detectados por el análisis. Las mejoras presentadas contribuyen al análisis en dos dimensiones: el análisis modular contribuye a la escabilidad de la técnica de análisis subyacente a TACO, mientras que la recuperación de contraejemplos facilita el uso de la herramienta, ocultando adecuadamente los detalles del método formal subyacente en su aplicación.