Certificación formal de programas en un lenguaje funcional impaciente
- Dios Castro, Javier de
- Ricardo Peña Marí Doktorvater/Doktormutter
Universität der Verteidigung: Universidad Complutense de Madrid
Fecha de defensa: 20 von Januar von 2012
- Narciso Martí Oliet Präsident/in
- Clara M. Segura Díaz Sekretär/in
- Víctor M. Gulías Vocal
- Jesús María Aransay Azofra Vocal
- Salvador Lucas Alba Vocal
Art: Dissertation
Zusammenfassung
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.