Defensa Tesis Doctorado Juan Pablo Galeotti

• Título: Verificación de Software usando Alloy
• Director: Marcelo Frias
• Jurados:
  
  Dr. Alfredo Olivero, Universidad Argentina de la Empresa.
  Dr. Darko Marinov, University of Illinois at Urbana-Champaign, USA.
  Dr. Daniel Jackson, Massachusetts Institute of Technology, USA.
• Resumen

La verificación acotada de software usando SAT consiste en la traducción del programa junto con las anotaciones provistas por el usuario a una fórmula proposicional. Luego de lo cual la fórmula es analizada en busca de violaciones a la especificación usando un SAT-solver. Si una violación es encontrada, una traza de ejecución exponiendo el error es exhibida al usuario.

Alloy es un lenguaje formal relacional que nos permite automáticamente analizar especificiaciones buscando contraejemplos de aserciones con la ayuda de un SAT-solver off-the-shelf.

En la presente tesis introducimos una técnica novedosa, general y complementamente automatizable para analizar programas Java secuenciales anotados con JML usando Alloy.

Esta técnica es especialmente beneficiosa cuando el programa opera con estructuras de datos complejas. Describiremos numerosos resultados experimentales que sostienen la pertinencia y eficacia del método presentado.