Análisis y Verificación de Programas (CC7126)

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:

• Semántica formal de programas: reconocerá dos estrategias clásicas para describir rigurosamente el significado o efecto de un programa.
• Verificación formal de programas: será capaz de demostrar (en el sentido matemático) la corrección funcional de un programa mediante el uso de lógica de Hoare y razonar también sobre programas que manipulan estructuras de datos dinámicas mediante el uso de lógica de separación.
• Análisis estático de programas: será capaz de razonar formalmente sobre propiedades más generales de los programas, de manera completamente automática, y en tiempo de compilación.

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.

• G. Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993 (disponible en biblioteca)
• F. Nielson et al., Semantics with Applications: An Appetizer, Springer, 2007 (disponible en biblioteca)
• F. Nielson et al., Principles of Program Analysis, Springer, 2015 (disponible en biblioteca)
• P.W. O'Hearn, A Primer on Separation Logic (and Automatic Program Verification and Analysis), Notas de la Escuela de Verano Marktoberdorf 2011 (disponible online)
• J. B. Almeida et al., Rigorous Software Development: An Introduction to Program Verification, Springer, 2011
• A. Appel et al., Program Logics for Certified Compilers, Cambridge University Press, 2014
• P. Cousot, A Tutorial on Abstract Interpretation, VMCAI'05 Industrial Day on Automatic Tools for Program Verification, 2005 (disponible online)

Federico Olmedo, Oficia 311N, email