Verificación formal de compiladores: Estudio de un caso

Ponente(s): Angel Francisco Zúñiga Chávez

Un compilador es una pieza fundamental hoy en día, pero como cualquier programa es susceptible de contener "bugs", de hecho la gran mayoría de compiladores en producción (como GCC) los tienen. Un error en un compilador podría introducir uno o varios errores en los archivos ejecutables que produce, lo que se traduce en diversas consecuencias negativas de alto impacto, como por ejemplo: pérdidas económicas y riesgos de salud (pensemos en una aplicación médica para manejar un láser en cirugías de humanos). Por ello consideramos que es imprescindible contar con compiladores correctos, más aun en el contexto de aplicaciones de misión crítica. Garantizar la corrección de un compilador es una tarea de gran importancia y puede verificarse formalmente en una computadora con ayuda de un asistente de demostración. En esta plática presentaremos el estudio del caso de un pequeño lenguaje funcional utilizando el asistente de demostración Coq.