Resumen:
TACO es una herramienta de análisis automático de programas. En este trabajo se presentan modificaciones a TACO para mejorar su escalabilidad y usabilidad, y proveer una mejor herramienta de análisis. Para realizar verificación de programas con ciclos, TACO utiliza loop unrolling como única técnica de resolución de los mismos. En este trabajo presentamos dos formas de utilizar invariantes de ciclo como alternativa al loop unrolling para mejorar la escalabilidad. Para comprobar el impacto en la escalabilidad se realizaron una serie de experimentos, analizando diferentes programas con los diferentes tipos de análisis. A partir de los resultados experimentales pudimos comprobar las mejoras de performance al utilizar los nuevos tipos de análisis frente al análisis utilizando loop unrolling. Finalmente, se presenta una herramienta de visualización de los contraejemplos encontrados por TACO, a fin de facilitar a los usuarios el análisis de los mismos para encontrar bugs en los programas que originaron dichos contraejemplos.
Citación:
---------- APA ----------
Bendersky, Pablo Gabriel. (2010). Hacia un entorno integrado para la verificación de contratos utilizando SAT solvers. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000436_Bendersky
---------- CHICAGO ----------
Bendersky, Pablo Gabriel. "Hacia un entorno integrado para la verificación de contratos utilizando SAT solvers". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2010.https://hdl.handle.net/20.500.12110/seminario_nCOM000436_Bendersky
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000436_Bendersky.pdf
Distrubución geográfica
