Defensa Tesis Licenciatura Ariel Neisen
Título: Verificación Automática de Estructuras de Datos Acíclicas usando Demostradores de Teoremas. Directores: Diego Garbervetsky y Daniel Gorín
| Qué |
|
|---|---|
| Cuándo |
27/04/2010 de 05:30 pm a 06:30 pm |
| Dónde | Aula 13. Pabellon 1 |
| Agregar evento al calendario |
vCal
iCal
|
- Título: Verificación Automática de Estructuras de Datos Acíclicas usando Demostradores de Teoremas
- Directores: Diego Garbervetsky y Daniel Gorín
- Jurado: Eduardo Bonelli y Guido de Caso
- Resumen
La técnica de "dynamic frames" (Kassios, 2006) utiliza variables de especificación especiales para resolver el problema conocido como "framing problem". Éste consiste en describir el alcance de los efectos de una función en presencia de memoria dinámica y aliasing. Recientemente, Leino (2008) mostró con el lenguaje Dafny cómo combinar "dynamic frames" con técnicas estándar de verificación estática.
En esta tesis mostramos que es posible reutilizar las variables de especificación introducidas para el "dynamic framing", de manera de poder garantizar estáticamente la aclicidad de referencias en el Heap, para clases anotadas por el usuario como tales. Es sabido que este tipo de propiedades estructurales sobre el Heap son difíciles de verificar estáticamente. Pusimos a prueba esta técnica extendiendo el lenguaje Dafny para que incorpore anotaciones de aciclicidad sobre clases.
