Los problemas en las piezas de software pueden acarrear consecuencias catastróficas, tanto a nivel económico como de la seguridad de las personas. La validación y verificación de software juegan, por lo tanto, un rol fundamental en el proceso de desarrollo. En particular, para el proceso de verificación se ha recurrido históricamente a diversas técnicas de testing. Si bien el testing representa un enfoque muy eficiente para detectar bugs, su alcance está limitado a probar la presencia de bugs, y no su ausencia.
En este curso estudiaremos el análisis y verificación formal de programas, que constituyen un conjunto de herramientas matemáticas para razonar formalmente sobre el comportamiento de los programas. A diferencia del testing, su empleo permite demostrar–en el sentido matemático–que los programas son correctos y se adhieren a su especificación.
A lo largo del curso presentaremos los fundamentos matemáticos subyacentes a dichas herramientas, reconociendo, en particular, sus alcances y limitaciones. Estudiaremos, además, las distintas estrategias que se utilizan para automatizar su aplicación.
Al término del curso, el estudiante manejará las nociones de:
Curso electivo para Doctorado en Computación, Magíster en Ciencias de la Computación e Ingeniería Civil en Computación.
CC4101 Lenguajes de Programación / Autorización (contactar Federico).
El curso no presenta ningún requisito adicional, aunque será de gran ayuda cierto grado de madurez matemática por parte del alumno.
Evaluación continua a través de tareas y una presentación oral (en base a un artículo o capítulo de libro). No habrá controles.
Federico Olmedo, Oficia 311N, email