• Inicio

    Introducción
    El objetivo del curso es aprender técnicas de análisis automático de modelos y de código. Estas técnicas permiten (por ejemplo) encontrar automáticamente ciertos bugs en especificaciones y en programas, mejorar su calidad/legibilidad e incluso a extraer información no trivial sobre el mismo, para entenderlo mejor, para comprender sus requisitos no funcionales, optimizarlo/transformarlo, etc.
     
    En este curso vamos a proveer los elementos básicos que les permitirán desarrollar sus propias herramientas de análisis o extender las existentes como así también introducirlos en un área de investigación muy activa.
     
    (*) Ojo que el nombre formal de la materia es para el sistema de inscripciones es: "Análisis y Modelado de Sistemas Reactivos". Anotense en esta. 
     
    Docentes
    Los profesores de la materia son:
    - Diego Garbervetsky -- http://lafhis.dc.uba.ar/~diegog
    - Victor Braberman -- http://lafhis.dc.uba.ar/~vbraber
    - Sebastian Uchitel -- http://lafhis.dc.uba.ar/~suchitel
     
    Estarán participando también algunos de los  docentes miembros del nuestro grupo de investigación: Guido de Caso, German Sibay, Esteban Pavese, Nicolas D'Ippolito y posiblemente otros miembros del grupo.
     
    Cursada
    La materia se va a cursar dos veces por semana (un total de 6hs. semanales), va a dar 3 puntos de optativa para la licenciatura y 4 puntos para doctorado. 
     
    La materia va a estar diseñada para que los que quieran luego hacer una tesis de licenciatura en estos temas puedan extender el trabajo realizado en la materia a una tesis.
     
    Con respecto a los horarios, se decidirán en función de las posibilidades de los interesados.
     
    Requisitos Lógica y Ingeniería de Software (prácticos).  Recomendamos tambien Paradigmas de Lenguajes de Programación y/o Teoría de Lenguajes pero no es excluyente.  
     

     
    Programa

    PARTE 1
     
    1)  Especificación de Sistemas Reactivos y Concurrentes.
         a. Algebras de Procesos y Automatas
                   - Congruencias, Refinamientos, Equivalencias
        b. Lógicas lineales y branch
        c. Teoría de modelos
        d. Herramienta: LTSA
    2) Verificación de Sistemas Reactivos y Concurrentes
         a. Model checking explícito para lógica lineal.
                   - Autómatas sobre lenguajes infinitos. Büchi
                   - Herramientas: LTSA
         b. Model checking simbólico de lógicas branching time.
                   - Reticulados y teorema de Tarski sobre puntos fijos.
                   - Verificación por punto fijo. Fairness
                   - Estructuras de datos para la verificación simbólica.
                   - Herramientas: nuSMV.

    PARTE 2

    3) Software Model Checking
         a. Software model checking explicito
         b. Fundamentos y técnicas para la verificación de propiedades de safety en código usando semántica operacional.
                   - Predicate Abstracción.
                   - Tratamiento de cadena de llamadas (lenguajes libres de contexto).
                   - Método CEGAR (counter example guided abstraction-refinement).
         c.     Herramienta: Blast
    4)    Verificación Estática de Contratos
         a. Fundamentos y técnicas para el análisis estático basada en semántica axiomática (tipo Hoare)
         b. Generación de condiciones de verificación
                   - Strongest y Weakest precondition
         c. Desafíos de los lenguajes OO.
         d. Demostradores automáticos de teoremas
                   - SMT y SAT solving
         e. Herramientas: SPEC# (C#+SMT),  ESCJAVA2 (Java+SMT), TACO (Java + SAT), Dafny
    5)    Inferencia automática de propiedades
         a. Data flow analysis
         b. Abstract interpretation
                   - Conexión de Galois
                   - Teorema Fundamental de la Aproximación
         c. Aplicaciones
                   - Detección de errores mecánicos (e.g. null pointers, división por cero, variables muertas)
                   - Points to analysis
                   - Generación invariantes
         d. Herramientas.
                   - Soot, Plural
                   - Code contracts.