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


==== Motivación y Objetivos  ====

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. 


==== Contenido  ====
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.


==== 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 [[folmedo@dcc.uchile.cl|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 ([[https://uchile-primo.hosted.exlibrisgroup.com/primo-explore/fulldisplay?docid=uchile_alma21142459530003936&context=L&vid=56UDC_INST&search_scope=uchile_scope&tab=uchile_tab&lang=es_CL|disponible en biblioteca]])
  * F. Nielson et al., //Semantics with Applications: An Appetizer//, Springer, 2007 ([[https://uchile-primo.hosted.exlibrisgroup.com/primo-explore/fulldisplay?docid=uchile_alma51170845280003936&context=L&vid=56UDC_INST&search_scope=uchile_scope&tab=uchile_tab&lang=es_CL|disponible en biblioteca]])
  * F. Nielson et al., //Principles of Program Analysis//, Springer, 2015 ([[https://uchile-primo.hosted.exlibrisgroup.com/primo-explore/fulldisplay?docid=uchile_alma21123471330003936&context=L&vid=56UDC_INST&search_scope=uchile_scope&isFrbr=true&tab=uchile_tab&lang=es_CL|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 ([[http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/Marktoberdorf11LectureNotes.pdf|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 ([[https://homepage.cs.uiowa.edu/~tinelli/classes/seminar/|disponible online]])


==== Contacto ====
Federico Olmedo, Oficia 311N, [[folmedo@dcc.uchile.cl|email]]