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:35] 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) ======
  
-==== ¿Por qué este curso?  ==== 
  
-==== Objetivos y contenido  ====+==== 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 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  ==== ==== 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  ====
 +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  ==== ==== Material  ====
Line 18: 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]]
 +