Título: Asistentes de prueba y verificación formal
26 de mayo
Conferencista: Lourdes del Carmen González Huesca
Resumen:
El uso de las computadoras para automatizar tareas es una práctica común, inclusive es posible realizar demostraciones matemáticas usando herramientas computacionales diseñadas para ello.
En esta plática veremos un acercamiento a la verificación formal dentro del área de Métodos Formales en Ciencias de la Computación y comentaremos los principios de los sistemas interactivos para el manejo de demostraciones que facilitan la verificación de sistemas y formalizaciones matemáticas.
En particular, nos enfocaremos en el asistente llamado Coq que también es considerado como un ambiente de desarrollo para la programación certificada.
Temas: