martes, 27 de noviembre de 2007

Defensa de tesis de licenciatura de Guido de Caso

Qué: Defensa de tesis de licenciatura
Quién: Guido de Caso
Cuándo: Martes 4 de diciembre a las 19hs.
Dónde: Aula a confirmar.

Título: "Construcciones de alto nivel como anotaciones para la verificación automática de software"

Directores: Diego Garbervetsky, Daniel Gorín
Jurado: Eduardo Bonelli, Juan Pablo Galeotti

Breve resumen:
"La verificación automática de software es una disciplina que ha crecido mucho en los últimos años, aportando herramientas que con bajo costo permiten aumentar la confianza que se tiene sobre un sistema. En particular la verificación automática de código ha comenzado a ser una alternativa viable, pero gran parte de las herramientas actuales se han montado sobre lenguajes preexistentes. Este enfoque ha brindado soluciones que pueden lidiar sólo con una parte del poder expresivo de los mismos y suelen ser introducidas mediante modificaciones ad-hoc a la sintaxis. Esta metodología no integral desfavorece la adopción de estas técnicas a gran escala.

Se presenta en este trabajo un lenguaje imperativo multiprocedural muy básico cuyo diseño está orientado a la verificabilidad. Se dota a este lenguaje de mecanismos de inferencia de precondiciones y postcondiciones que permiten asistir la tarea de anotar ciertos fragmentos del código. Haciendo uso de estas técnicas se extiende el lenguaje con construcciones de iteración de alto nivel para las cuales no es necesario proveer ningún tipo de anotación para su verificación. Se espera que estas característiscas alivien la carga de trabajo que requiere especificar un programa, logrando de esta forma una adopción mayor de las técnicas de verificación automática. Se presenta un prototipo de herramienta que pone a prueba esta hipótesis, trabajando con un conjunto diverso de demostradores de teoremas en paralelo de forma tal de maximizar la cantidad de programas que pueden ser verificados sin intervención del programador."

Como parte de la defensa se hará una breve demostración del prototipo de herramienta implementado.

¡Quedan todos cordialmente invitados!

No hay comentarios.: