1. Inicio
  2. Atrás
Título: Análisis modular y recuperación de contraejemplos en TACO
Autores: Alborodo, Raúl
Ricci, Nicolás
Galeotti, Juan P.
Aguirre, Nazareno Matías
Fecha: 2012-07-19
2011-10
2011
Publicador: Unversidad Nacional de La Plata
Fuente:

Tipo: Objeto de conferencia
Objeto de conferencia
Tema: Software/Program Verification
Languages
Ciencias Informáticas
Descripción: 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.
Presentado en el II Workshop Aspectos Teóricos de Ciencia de la Computación (WATCC)
Idioma: Español