Demostraciones asistidas por computadoras y Programación certificada

Ponente(s): Lourdes Del Carmen González Huesca

En esta plática daremos un acercamiento a la verificación formal dentro del área de métodos formales en Ciencias de la Computación. Iniciaremos con un panorama de las herramientas para la correción de programas y su utilidad. Después se revisarán las herramientas que ofrecen mayores ventajas para la corrección total de programas: los asistentes de prueba. Finalmente, nos enfocaremos en uno de los asistentes más usados llamado Coq como un ambiente de desarrollo para la programación certificada.