Diagrama de temas

  • Inicio

    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: Lunes de 17:00 a 22:00 hs.
    • Laboratorios: 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
    • Cursada

      • Teoricas: Lunes 17hs a 22hs - Aula 13
      • Practicas/Laboratorio: Jueves 17hs a 22hs - Labo 1
      • Docentes

        Lista para consultas, comentarios:
            ingsoft2-doc(A)dc.uba.ar

        Lista para alumnos:
            ingsoft2-alu(A)dc.uba.ar

        ----------------------------------------------------------------

        Profesor

        • Dr. Victor Braberman [vbraber(A)dc.uba.ar]

        Jefes de Trabajos Prácticos

        • Dr. Daniel Ciolek [dciolek(A)dc.uba.ar]

        Ayudantes de Primera

        • Lic. Leandro Nahabedian [lnahabedian(A)dc.uba.ar]
        • Lic. Virginia Brassesco [mbrassesco(A)dc.uba.ar]
        • Calendario

          • Ejercicios Adicionales

          • Bibliografía

            • Jeff Magee and Jeff Kramer. 2000. Concurrency: State Models &Amp; Java Programs. John Wiley & Sons, Inc., New York, NY, USA.
            • Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 2000. Model Checking. MIT Press, Cambridge, MA, USA.
            • Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press.