Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
teaching:cc7126 [2018/01/31 11:13]
folmedo
teaching:cc7126 [2018/01/31 15:19] (current)
folmedo
Line 2: Line 2:
  
  
-==== ¿Por qué este curso?  ====+==== Motivación y Objetivos  ====
  
-==== Objetivos contenido  ==== +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//.  
-Al término del cursoel 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: +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.    * **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.   * **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.   * **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 ==== ==== Elegibilidad ====