Registro:
| Documento: | Tesis de Grado |
| Título: | Análisis de dataflow para mejorar la verificación de programas basada en SAT |
| Autor: | Cuervo Parrino, Bruno Esteban |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2024-08-30 |
| Fecha de defensa: | 2011-05-20 |
| Fecha en portada: | Mayo 2011 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Galeotti, Juan Pablo |
| Director Asistente: | Garbervetsky, Diego David |
| Jurado: | Pavese, Esteban; López Pombo, Carlos Gustavo |
| Idioma: | Español |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000514_CuervoParrino |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000514_CuervoParrino.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000514_CuervoParrino |
| Ubicación: | Dep.COM 000514 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Cuervo Parrino, Bruno Esteban. (2011). Análisis de dataflow para mejorar la verificación de programas basada en SAT. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000514_CuervoParrino |
Resumen:
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.
Citación:
---------- APA ----------
Cuervo Parrino, Bruno Esteban. (2011). Análisis de dataflow para mejorar la verificación de programas basada en SAT. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000514_CuervoParrino
---------- CHICAGO ----------
Cuervo Parrino, Bruno Esteban. "Análisis de dataflow para mejorar la verificación de programas basada en SAT". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2011.https://hdl.handle.net/20.500.12110/seminario_nCOM000514_CuervoParrino
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000514_CuervoParrino.pdf
Distrubución geográfica
