Encabezado Facultad de Ciencias
Presentación

Ciencias de la Computación (plan 1994) 2013-1

Optativas, Seminario de Computación Teórica II

Grupo 7033, 20 lugares. 7 alumnos.
Especificación formal y certificación de programas con COQ
Profesor Favio Ezequiel Miranda Perea lu mi vi 10 a 11 Taller de Lenguajes de Programación
Ayudante Araceli Liliana Reyes Cabello ma ju 10 a 11 Taller de Lenguajes de Programación
Ayud. Lab.

 

A PETICION DE LOS INTERESADOS EL HORARIO CAMBIA DE 10 A 11 EN EL TALLER DE LENGUAJES DE PROGRAMACION A PARTIR DEL MIERCOLES 8 DE AGOSTO.

La confiabilidad de diversos sistemas de cómputo juega actualmente un papel muy relevante en nuestra sociedad. Proyectos recientes de software en la industria ya no se limitan a producir código, sino que la obtención de código certificado se ha vuelto una necesidad crucial. Esta certificación es en relación a la especificación de funcionalidades o propiedades de ejecución, como por ejemplo la restricción al acceso a recursos no autorizados o simplemente asegurar que el propósito del software sea el esperado.

Una manera formal de certificar programas, cada vez más común en aplicaciones reales, es mediante el uso de asistentes de prueba.
Los asistentes de prueba permiten construir pruebas matemáticas susceptibles de verificarse de forma algorítmica, proporcionando así
un nivel mucho más alto de confiabilidad que la verificación tradicional hecha por humanos. El uso de estos asistentes crece dia a dia y sus aplicaciones van
desde la demostración de teoremas matemáticos hasta el desarrollo de pruebas de correctud de software ejecutable con respecto a su especificación.

El objetivo de este seminario es dar una introducción al uso de métodos formales para la especificación y certificación de programas mediante el asistente de prueba Coq (http://coq.inria.fr/), mostrando así que es posible desarrollar software correcto por construcción utilizando razonamiento formal, software que por lo tanto no requiere de un proceso adicional de verificación.

Prerrequisitos: Indispensable Análisis Lógico, deseable: lenguajes de programación.

Evaluación:

El seminario se calificará exclusivamente con tareas, prácticas y proyecto final.

Temario:

1. Introducción y panorama de un ejemplo completo (Certificación de un compilador)
2. Programación funcional: expresiones,tipos y estructuras de datos en Coq.
3. Lógica: proposiciones y pruebas.
4. Polimorfismo, funciones de orden superior y tipos dependientes.
5. Tácticas.
6. Definiciones inductivas.
7. Extracción de programas certificados.
8. Estudio de casos particulares.

La página del curso está aquí: https://sites.google.com/site/unamfcsct131

 


Hecho en México, todos los derechos reservados 2011-2016. Esta página puede ser reproducida con fines no lucrativos, siempre y cuando no se mutile, se cite la fuente completa y su dirección electrónica. De otra forma requiere permiso previo por escrito de la Institución.
Sitio web administrado por la Coordinación de los Servicios de Cómputo de la Facultad de Ciencias. ¿Dudas?, ¿comentarios?. Escribenos. Aviso de privacidad.