Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
teaching:cc7126 [2018/01/31 10:50] folmedoteaching:cc7126 [2018/01/31 15:19] (current) folmedo
Line 1: Line 1:
 ====== Análisis y Verificación de Programas (CC7126) ====== ====== Análisis y Verificación de Programas (CC7126) ======
-**Curso electivo para Doctorado en Computación, Magíster en Ciencias de la Computación e Ingeniería Civil en Computación** 
  
  
-==== ¿Por qué este curso ====+==== 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.
  
-==== Objetivos y contenido  ==== 
  
 ==== Requisitos  ==== ==== Requisitos  ====
-CC4101 Lenguajes de Programación / Autorización.\\ El curso no presenta ningún requisito adicional, aunque será de gran ayuda  cierto grado de madurez matemática por parte del alumno.+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.
  
  
Line 24: Line 39:
   * A. Appel et al., //Program Logics for Certified Compilers//, Cambridge University Press, 2014   * 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]])   * 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]]
 +