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

Al término del curso, el estudiante tendrá un dominio general sobre las diferentes técnicas empleadas en la análisis y verificación formal de programas. El estudiante estará familiarizado con los fundamentos matemáticos subyacentes a cada una de dichas técnicas, reconociendo, en particular, sus alcances y limitaciones. El estudiante estará familiarizado, además, con los algoritmos y estrategias tradicionalmente utilizados para mecanizar dichas técnicas. El estudiante que apruebe el curso 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