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

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

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Alborodo, Raúl, Ricci, Nicolás, Galeotti, Juan P., Aguirre, Nazareno Matías
Formato: Objeto de conferencia
Lenguaje:Español
Publicado: 2011
Materias:
Ciencias Informáticas
Software/Program Verification
Languages
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/18789
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-18789
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Español
topic Ciencias Informáticas
Software/Program Verification
Languages
spellingShingle Ciencias Informáticas
Software/Program Verification
Languages
Alborodo, Raúl
Ricci, Nicolás
Galeotti, Juan P.
Aguirre, Nazareno Matías
Análisis modular y recuperación de contraejemplos en TACO
topic_facet Ciencias Informáticas
Software/Program Verification
Languages
description 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.
format Objeto de conferencia
Objeto de conferencia
author Alborodo, Raúl
Ricci, Nicolás
Galeotti, Juan P.
Aguirre, Nazareno Matías
author_facet Alborodo, Raúl
Ricci, Nicolás
Galeotti, Juan P.
Aguirre, Nazareno Matías
author_sort Alborodo, Raúl
title Análisis modular y recuperación de contraejemplos en TACO
title_short Análisis modular y recuperación de contraejemplos en TACO
title_full Análisis modular y recuperación de contraejemplos en TACO
title_fullStr Análisis modular y recuperación de contraejemplos en TACO
title_full_unstemmed Análisis modular y recuperación de contraejemplos en TACO
title_sort análisis modular y recuperación de contraejemplos en taco
publishDate 2011
url http://sedici.unlp.edu.ar/handle/10915/18789
work_keys_str_mv AT alborodoraul analisismodularyrecuperaciondecontraejemplosentaco
AT riccinicolas analisismodularyrecuperaciondecontraejemplosentaco
AT galeottijuanp analisismodularyrecuperaciondecontraejemplosentaco
AT aguirrenazarenomatias analisismodularyrecuperaciondecontraejemplosentaco
bdutipo_str Repositorios
_version_ 1764820463268134913

Ejemplares similares