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 13:18] folmedoteaching:cc7126 [2018/01/31 15:19] (current) folmedo
Line 2: Line 2:
  
  
-==== ¿Por qué este curso?  ==== +==== Motivación y Objetivos  ====
-**Testing shows the presence, not the absence of bugs    --Edsger W. Dijkstra** +
  
 +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. 
  
-==== Objetivos y contenido  ==== +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.  
-Al término del curso, el 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: + 
 +==== 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 ====