Ciencias de la Computación (plan 1994) 2014-2

Optativas, Semántica y Verificación

Sinopsis:

El análisis y la verificación de sistemas de software es un asunto importante. Los errores en sistemas cuya seguridad es crítica pueden ser desastrosos causando pérdidas financieras enormes o incluso la muerte, por lo que los métodos para evitar estos escenarios son esenciales. Un proceso de pruebas preliminares puede identificar problemas, si se realiza de manera rigurosa, pero por lo general no es suficiente para garantizar un nivel satisfactorio de calidad. Por otra parte la teoría de especificación y verificación formal ofrece metodologías que van desde la descripción formal de requerimientos, lo cual permite razonar rigurosamente sobre ellos, hasta sofisticadas técnicas automátizadas para la verificación de software. El objetivo de este curso es proporcionar un panorama de algunos métodos de especificación y verificación formal mediante el estudio de casos en semánticas formales de lenguajes de programación, haciendo énfasis en el proceso de verificación automatizada mediante el uso del asistente de prueba Coq (http://coq.inria.fr )

La página del curso está aquí

Aviso importante: las clases de lunes y miércoles serán en el salón 301, tercer piso del edificio anexo al IIMAS, mismo lugar de la coordinación del Posgrado en Computación.