This is an old revision of the document!


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

¿Por qué este curso?

Objetivos y contenido

Elegibilidad

Curso electivo para Doctorado en Computación, Magíster en Ciencias de la Computación e Ingeniería Civil en Computación.

Requisitos

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

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.

Material

  • 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)

Contacto

Federico Olmedo, Oficia 311N, Email