Los métodos formales para la verificación de software son un área fundamental de las ciencias de la
computación. A través de modelos lógico-matemáticos se establece un vínculo (a través de una
demostración formal) que un programa cumple con una especificación. Los asistentes de pruebas son un
conjunto de herramientas que hacen posible verificar la corrección de programas en un entorno de software. En
general, trabajan con lógicas de alto poder expresivo, y por lo tanto no decidibles. En el curso se trabaja sobre
un asistente de pruebas que permite expresar, a través de la correspondencia de Curry-Howard, pruebas y
programas en el mismo formalismo matemático. A lo largo del curso se destaca la importancia de la
construcción formal de programas con aplicaciones a sistemas crítcos.

Profesor: Carlos Luna - Dante Zanarini
Sitio alternativo: https://eva.fing.edu.uy/course/view.php?id=363