Análisis de dataflow para mejorar la verificación de programas basada en SAT

Mostrar todas las versiones(2)

La verificación acotada de programas basada en SAT-solving 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-so...

Descripción completa

Detalles Bibliográficos
Autor principal:	Cuervo Parrino, Bruno Esteban
Otros Autores:	Galeotti, Juan Pablo
Formato:	Tesis de grado publishedVersion
Lenguaje:	Español
Publicado:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2011
Materias:	BOUNDED PROGRAM VERIFICATION DATAFLOW ANALYSIS SAT SOLVING
Acceso en línea:	https://hdl.handle.net/20.500.12110/seminario_nCOM000514_CuervoParrino
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	seminario:seminario_nCOM000514_CuervoParrino
record_format	dspace
spelling	seminario:seminario_nCOM000514_CuervoParrino2025-05-09T18:45:44Z Análisis de dataflow para mejorar la verificación de programas basada en SAT Cuervo Parrino, Bruno Esteban Galeotti, Juan Pablo Garbervetsky, Diego David BOUNDED PROGRAM VERIFICATION DATAFLOW ANALYSIS SAT SOLVING La verificación acotada de programas basada en SAT-solving 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 programas Java con anotaciones JML a Alloy, un lenguaje formal relacional que permite analizar automáticamente especificaciones buscando contra ejemplos de aserciones con la ayuda de un SAT-solver. TACO introduce una técnica para computar los posibles valores asignados a las variables del programa, que llamamos cotas, en el estado inicial del programa. En esta tesis mostramos cómo las técnicas de dataflow, típicamente utilizadas por los compiladores para optimizar programas, 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 tanto la verificación de casos de estudio que no podían ser analizados anteriormente como, en algunos casos, la extensión del scope del análisis. Fil: Cuervo Parrino, Bruno Esteban. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2011-05-20 info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion application/pdf spa info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000514_CuervoParrino
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language	Español
orig_language_str_mv	spa
topic	BOUNDED PROGRAM VERIFICATION DATAFLOW ANALYSIS SAT SOLVING
spellingShingle	BOUNDED PROGRAM VERIFICATION DATAFLOW ANALYSIS SAT SOLVING Cuervo Parrino, Bruno Esteban Análisis de dataflow para mejorar la verificación de programas basada en SAT
topic_facet	BOUNDED PROGRAM VERIFICATION DATAFLOW ANALYSIS SAT SOLVING
description	La verificación acotada de programas basada en SAT-solving 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 programas Java con anotaciones JML a Alloy, un lenguaje formal relacional que permite analizar automáticamente especificaciones buscando contra ejemplos de aserciones con la ayuda de un SAT-solver. TACO introduce una técnica para computar los posibles valores asignados a las variables del programa, que llamamos cotas, en el estado inicial del programa. En esta tesis mostramos cómo las técnicas de dataflow, típicamente utilizadas por los compiladores para optimizar programas, 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 tanto la verificación de casos de estudio que no podían ser analizados anteriormente como, en algunos casos, la extensión del scope del análisis.
author2	Galeotti, Juan Pablo
author_facet	Galeotti, Juan Pablo Cuervo Parrino, Bruno Esteban
format	Tesis de grado Tesis de grado publishedVersion
author	Cuervo Parrino, Bruno Esteban
author_sort	Cuervo Parrino, Bruno Esteban
title	Análisis de dataflow para mejorar la verificación de programas basada en SAT
title_short	Análisis de dataflow para mejorar la verificación de programas basada en SAT
title_full	Análisis de dataflow para mejorar la verificación de programas basada en SAT
title_fullStr	Análisis de dataflow para mejorar la verificación de programas basada en SAT
title_full_unstemmed	Análisis de dataflow para mejorar la verificación de programas basada en SAT
title_sort	análisis de dataflow para mejorar la verificación de programas basada en sat
publisher	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate	2011
url	https://hdl.handle.net/20.500.12110/seminario_nCOM000514_CuervoParrino
work_keys_str_mv	AT cuervoparrinobrunoesteban analisisdedataflowparamejorarlaverificaciondeprogramasbasadaensat
_version_	1831983616936116224

Análisis de dataflow para mejorar la verificación de programas basada en SAT

Ejemplares similares