Certificación formal de programas en un lenguaje funcional impaciente

• Autores: Javier de Dios Castro
• Directores de la Tesis: Ricardo Peña Marí (dir. tes.)
• Lectura: En la Universidad Complutense de Madrid ( España ) en 2012
• Idioma: español
• Tribunal Calificador de la Tesis: Narciso Martí Oliet (presid.) , Clara M. Segura Díaz (secret.) , Jesús María Aransay Azofra (voc.) , Salvador Lucas Alba (voc.) , Víctor M. Gulías (voc.)
• Texto completo no disponible (Saber más ...)
• Resumen

  • 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.