Differences

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

--- teaching:cc7126 [2018/01/31 15:12] – folmedo
+++ teaching:cc7126 [2018/01/31 19:19] (current) – folmedo
@@ Line 2: / Line 2: @@
-==== ¿Por qué este curso?  ====
+==== Motivación y Objetivos  ====
-==== Objetivos y 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 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.