Tesis doctoral de JavierDe Dios Castro
En esta tesis se propone un metodo basado en la infraestructura pcc para convertir las anotaciones inferidas por los análisis estáticos del compilador del lenguaje safe, un lenguaje funcional impaciente, en demostraciones comprobables automáticamente mediante el demostrador asistido de teoremas isabelle/hol, permitiendo certificar ciertas propiedades en los programas. Estas propiedades son la ausencia de punteros descolgados y las cotas de memoria seguras.
Datos académicos de la tesis doctoral «Certificación formal de programas en un lenguaje funcional impaciente«
- Título de la tesis: Certificación formal de programas en un lenguaje funcional impaciente
- Autor: JavierDe Dios Castro
- Universidad: Complutense de Madrid
- Fecha de lectura de la tesis: 20/01/2012
Dirección y tribunal
- Director de la tesis
- Ricardo Peña Marí
- Tribunal
- Presidente del tribunal: narciso Martí oliet
- victor m. Gulias fernandez (vocal)
- Jesús María Aransay azofra (vocal)
- salvador Lucas alba (vocal)