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!

¡Diego es doctor!

¡Hoy (o mejor dicho ayer) diego se doctoró! Ahora tiene mucho tiempo libre para ayudarme a terminar de revisar mi tesis ;).

Hablando de lo cual, en estos días estuve terminando de escribir los capítulos 5 y 6. Si todo marcha bien se los mandamos al jurado la semana que viene.

Estuvimos hablando con Diego sobre fechas para presentar la tesis. Una posibilidad sería martes 11 de diciembre... veremos si el jurado llega a revisar toda la tesis para ese entonces. ¡Ojalá así sea!

Jurado con capítulos

El jurado, compuesto por Juan Pablo Galeotti y Eduardo Bonelli, recibió el viernes una copia de los primeros cuatro capítulos de mi tesis.

Mientras ellos avanzan en su lectura, yo continúo escribiendo lo que falta.

Cuatro adentro

Hace instantes les mandé a Diego y a Dani los primeros 4 capítulos de la tesis. En teoría ya tienen todos los cambios que ellos me sugirieron. De esta forma, si todos los planetas se alinean, le estaría mandando mañana (viernes) al jurado estos primeros 4 capítulos.

Faltan todavía terminar algunas partecitas del capítulo 5 y escribir las conclusiones y el future work para el capítulo 6. No falta tanto...

Un informe de nunca acabar

Sigo escribiendo el informe de la tesis. Se podría decir que los capítulos 1, 2 y 3 están bastante bien. El capítulo 4 está terminado pero tiene que atravezar varios procesos de revisión. El capítulo 5 está a medio escribir y el capítulo 6 (las conclusiones) todavía no lo empecé.

No falta tanto, pero no veo la hora de terminar, siempre aparece alguna cosa para corregir... ¡¡ánimo!!

Elecciones, Bariloche, introducción

La semana del 24/9 al 29/9 fue caótica. Elecciones, o sea pasarse las 25 horas del día en la facu, comiendo mal, durmiendo peor y mordiéndose las uñas...

Para descansar y aprovechando la oportunidad me escapé un par de días a Bariloche, lo cual me sirvió mucho para descansar.

Hoy, recién vuelto y con pilas renovadas, escribí el capítulo de introducción. También charle con Dani, que dentro de poco se va para Francia por unos meses.

Un paso atras, ¿dos adelante?

Dicen que a veces para dar avanzar hay que retroceder un poco. Puede que haya sido el caso esta semana.

El miércoles casi desespero cuando encontré un error que hizo tambalear varias partes relativamente importantes del formalismo que estamos usando.

Me pasé el jueves y el viernes sufriendo para ver como se emparchaba. Charlando con Diego y Dani para solucionarlo.

Finalmente la solución que encontramos no es la que más nos satisface, pero es la más cercana a lo que hay hecho. Cualquier otra versión que se nos ocurrió tenía problemas iguales o peores y nada parecía indicar que valía la pena el esfuerzo y el riesgo.

Así que casi como al comienzo, pero con muchas más justificaciones de por qué hicimos lo que hicimos cómo lo hicimos.