Objetivo
En esta materia se estudiarán algoritmos, estructuras de datos, técnicas y herramientas que apuntan a analizar software automáticamente. Prácticamente todos los análisis interesantes (que serían de utilidad para un ingeniero de software que desea garantías sobre el comportamiento de lo que está construyendo) son indecidibles o computacionalmente intratables. Por lo tanto lo que se estudiará en clase es el estado del arte en materia de análisis y verificación automática, un área que a pesar de estar dando pasos agigantados, aún tiene mas preguntas abiertas que respuestas.
Correlativas
- Ingeniería del Software 1 nueva
- Sistemas Operativos
- Paradigmas de Lenguajes de Programación
Horarios
A menos que el calendario indique lo contrario, las teóricas y prácticas se darán en los siguientes horarios:
- Teóricas, prácticas y consultas: Lunes de 17:00 a 22:00 hs.
- Teóricas, prácticas y consultas: Jueves de 17:00 a 22:00 hs.
Las fechas de los eventos importantes de la materia figuran en el calendario.
Programa
- Modelos de Concurrencia
- Algebras de Proceso y Bisimulación
- Lógicas temporales. LTL y CTL
- Model Checking de LTL y CTL
- Bounded Model Checking
- Predicate abstraction
- Docente: Fernando Asteasuain
- Docente: Victor Adrian Braberman
- Docente: Maria Virginia Brassesco
- Docente: Daniel Alfredo Ciolek
- Docente: Fernan Gabriel Martinelli
- Docente: Javier Ignacio Martinez Viademonte
- Docente: Leandro Ezequiel Nahabedian
- Docente: Sebastian Uchitel