Differences

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

Link to this comparison view

Next revision		Previous revision
Next revisionBoth sides next revision
teaching:cc7126 [2018/01/31 10:19] – created folmedoteaching:cc7126 [2018/01/31 13:18] – 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?  ==== ==== ¿Por qué este curso?  ====
 +**Testing shows the presence, not the absence of bugs    --Edsger W. Dijkstra** 
 +
 +
  
 ==== Objetivos y contenido  ==== ==== Objetivos y contenido  ====
 +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: 
 +  * **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  ====
  
-  * G. Winskel, //The Formal Semantics of Programming Languages//, MIT Press, 1993 +  * G. Winskel, //The Formal Semantics of Programming Languages//, MIT Press, 1993 ([[https://uchile-primo.hosted.exlibrisgroup.com/primo-explore/fulldisplay?docid=uchile_alma21142459530003936&context=L&vid=56UDC_INST&search_scope=uchile_scope&tab=uchile_tab&lang=es_CL|disponible en biblioteca]]) 
-  * F. Nielson et al., //Semantics with Applications: An Appetizer//, Springer, 2007 +  * F. Nielson et al., //Semantics with Applications: An Appetizer//, Springer, 2007 ([[https://uchile-primo.hosted.exlibrisgroup.com/primo-explore/fulldisplay?docid=uchile_alma51170845280003936&context=L&vid=56UDC_INST&search_scope=uchile_scope&tab=uchile_tab&lang=es_CL|disponible en biblioteca]]) 
-  * F. Nielson et al., //Principles of Program Analysis//, Springer, 2015 +  * F. Nielson et al., //Principles of Program Analysis//, Springer, 2015 ([[https://uchile-primo.hosted.exlibrisgroup.com/primo-explore/fulldisplay?docid=uchile_alma21123471330003936&context=L&vid=56UDC_INST&search_scope=uchile_scope&isFrbr=true&tab=uchile_tab&lang=es_CL|disponible en biblioteca]]) 
-  * P.W. O'Hearn, //A Primer on Separation Logic (and Automatic Program Verification and Analysis)//, Notas de la Escuela de Verano Marktoberdorf 2011+  * P.W. O'Hearn, //A Primer on Separation Logic (and Automatic Program Verification and Analysis)//, Notas de la Escuela de Verano Marktoberdorf 2011 ([[http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/Marktoberdorf11LectureNotes.pdf|disponible online]])
   * J. B. Almeida et al., //Rigorous Software Development: An Introduction to Program Verification//, Springer, 2011   * J. B. Almeida et al., //Rigorous Software Development: An Introduction to Program Verification//, Springer, 2011
   * 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+  * 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]]