Certificación formal de programas en un lenguaje funcional impaciente

  1. Dios Castro, Javier de
Zuzendaria:
  1. Ricardo Peña Marí Zuzendaria

Defentsa unibertsitatea: Universidad Complutense de Madrid

Fecha de defensa: 2012(e)ko urtarrila-(a)k 20

Epaimahaia:
  1. Narciso Martí Oliet Presidentea
  2. Clara M. Segura Díaz Idazkaria
  3. Víctor M. Gulías Kidea
  4. Jesús María Aransay Azofra Kidea
  5. Salvador Lucas Alba Kidea
Saila:
  1. Sistemas Informáticos y Computación

Mota: Tesia

Teseo: 113737 DIALNET

Laburpena

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.