Quinta Jornada de Doctorandos de Computación
FaMAF, Universidad Nacional de Córdoba

10 de Diciembre, 2014

Aula Magna, FAMAF





Introducción

Esta es la quinta Jornada de Doctorandos de Computación de la Facultad de Matemática, Astronomía y Física (FaMAF).

En esta jornada, los estudiantes del Doctorado en Ciencias de la Computación de FaMAF expondrán sus intereses de investigación y los aspectos más relevantes de su trabajo.

Este año además, contaremos con charlas a cargo de recientes doctores y/o investigadores de la FaMAF, que expondrán los intereses de cada grupo de investigación de la facultad

Uno de los principales objetivos de la jornada es dar a conocer las líneas de investigación que los doctorandos de Computación del FaMAF están desarrollando, y las posibles líneas de investigación posibles dentro de la facultad. Por eso invitamos a todos los alumnos y docentes (no sólo a los de Computación) a concurrir.

Participantes Confirmados ^

Acá ponemos la lista de todos los doctorandos que participan de las jornadas, en orden alfabético y con e-mail. Así el que esté interesado los puede buscar y/o/implica/forall contactar.
  • Carlos Budde (cbudde@famaf.unc.edu.ar)
  • Cristian Cardellino (crscardellino@gmail.com)
  • Renzo Degiovanni (rdegiovanni@dc.exa.unrc.edu.ar)
  • Emmanuel Gunther (manu.gunther@gmail.com)
  • Sonia Permigiani (spermigiani@gmail.com)
  • Nicolás Ricci (nricci.02@gmail.com)
  • Leonardo Rodríguez (leonardomatiasrodriguez@gmail.com)

Grupos Confirmados ^

En esta lista, ponemos el nombre y el e-mail de los expositores, juntos con los links a las páginas web de los grupos de investigación en Ciencias de la Computación de la FaMAF.

Programa del Evento ^

Horario Charla
09:20 Apertura
09:30 Carlos Budde
10:00 Emmanuel Gunther
10:30 Nicolás Ricci
11:00 Café
11:30 Renzo Degiovanni (Seminario)
12:15 Nicolás Wolovick/Carlos Bederián [Grupo GPGPU Computing]
12:30 Miguel Pagano [Grupo Semántica de la Programación]
12:45 Almuerzo
14:30 Leonardo Rodríguez
15:00 Cristian Cardellino
15:30 Raul Fervari [Grupo Lógicas, Interacción y Sistemas Inteligentes]
15:45 Juan Durán [Grupo Ingeniería de la Interacción Hombre-Máquina.]
16:00 Café
16:30 Sonia Permigiani (Seminario)
17:15 Franco Luque [Grupo Procesamiento de Lenguaje Natural]
17:30 Jorge Sánchez [Grupo Visión por Computadoras]
17.45 Matias Lee [Grupo Sistemas Confiables]
18.00 Cervezas en el bar de enfrente
  • Título: ¿Cual es la probabilidad de que se muera un obispo?
    Expositor: Carlos Budde
    Resumen: Al modelar sistemas, por ejemplo computacionales, es común preguntarse cosas como "¿es posible que se rompa todo?", o sino también "¿cuán seguido ocurre eso?", o bien "¿qué probabilidad hay de que ocurra mientras lo uso?" Herramientas como el model-checking pueden darnos respuestas de forma eficiente y confiable, siempre y cuando no pidamos demasiado. Si el sistema está adecuadamente preparado y "se resiste a romperse", las chances de observar las fallas buscadas se tornan bajas, y el evento se vuelve raro. En esta charla se discutirá brevemente una opción para tratar con dichos eventos raros, estimando su probabilidad de forma eficiente. De importancia principalmente cuando el presupuesto no alcanza para contratar al sicario.

  • Título: De Lenguaje Natural a Linked Data
    Expositor: Cristian Cardellino
    Resumen: El marco de trabajo de mi doctorado son métodos y técnicas orientadas a facilitar el mapping entre información expresada en lenguaje natural y linked data [0] (por ejemplo, una representación de la wikipedia como grafo RDF [1] ). Con este horizonte, he estado trabajando en tres líneas:
    • Traducción de preguntas a queries, dentro del marco de Quepy [2] . Mi objetivo fue aumentar cobertura y profundidad del análisis lingüístico de las preguntas. Con ese objetivo exploré la integración de información profunda asociada a los verbos dentro de Quepy.
    • Aprendizaje activo, para mejorar la calidad y cobertura de los modelos inferidos a partir de ejemplos analizados manualmente. Inicialmente exploré la técnica más simple, un método de aprendizaje iterativo llamado bootstrapping, aplicado a desambiguación de sentidos verbales. El objetivo era aumentar la información asociada a verbos que usamos en el punto anterior. He seguido avanzando en esta línea, pasando de este aprendizaje semisupervisado a aprendizaje activo. En el aprendizaje activo optimizamos la intervención del especialista que analiza manualmente los ejemplos (human in the loop) para maximizar la utilidad de cada ejemplo en el modelo aprendido.
    • Traducción de texto libre a ontologías RDF, mediante la mejora de la herramienta NLL2RDF [3] , orientada a obtener un grafo RDF de textos normativos, más concretamente, textos de licencias. Originalmente esta herramienta estaba basada en un clasificador supervisado, al cual hemos agregado elementos de aprendizaje a ctivo para mejorar cobertura de clasificación y aumentar la performance del clasificador original.


  • Título: Técnicas Automáticas para el Análisis de Requisitos de Software
    Expositor: Renzo Degiovanni
    Resumen: Es ampliamente aceptado que los errores son más fáciles (y menos costosos) de corregir si se capturan lo más temprano posible en el proceso de desarrollo. Luego, obtener una especificación de requisitos de buena calidad, es de fundamental importancia práctica y económica en la mayoría de las metodologías de desarrollo de software modernas. Esto motivó a que las notaciones formales para la especificación de requisitos adquirieran mayor atención en las últimas décadas. En este seminario, presentaré algunas de las técnicas automáticas desarrolladas durante mi doctorado. Dichas técnicas brindan soporte al proceso de elaboración y validación de requisitos de software. En breve, éstas se basan en manipulaciones de formulas lógicas, explotando la eficiencia de varios mecanismos de análisis provenientes de los métodos formales, como SAT solving, model checking e interpolación.

  • Título: ¿Cómo construir software correcto?
    Expositor: Emmanuel Gunther
    Resumen: Un programa de computación se escribe a partir de una especificación y luego se asume que su ejecución la satisfará. En general esta asunción es injustificada: La mayoría de los programas no satisfacen la especificación. Un enfoque deseable para la construcción de programas es tener un sistema en el cual la forma de escribir un programa permita asegurar propiedades antes de que el mismo sea ejecutado. En esta mini-charla daremos un pequeño vistazo a una clase de lenguajes de programación que permiten obtener este enfoque.

  • Título: Análisis Automático de Programas basados en Lógica de Separación
    Expositor: Sonia Permigiani
    Resumen: La lógica de separación es una extensión de lógica de Hoare que facilita el razonamiento acerca de la corrección de programas que hacen uso de memoria dinámica. La característica más destacada de la lógica de separación respecto de la lógica de Hoare convencional es la provisión de un operador de conjunción especial, que permite predicar sobre la estructura de la memoria utilizada por un programa descomponiendo la misma en regiones disjuntas, lo que permite un elegante tratamiento de aliasing de punteros. Desde la introducción de la lógica de separación hace más de diez años, muchas herramientas de análisis de software han sido desarrolladas basadas en este formalismo. En este seminario describiremos los conceptos fundamentales de la lógica de separación, y cómo este formalismo se incorpora y se utiliza en herramientas de análisis de software. Más aún, discutiremos diferentes aspectos que han afectado al formalismo original como consecuencia de su incorporación en herramientas de análisis concretas, en particular relacionados a limitaciones de expresividad. Compararemos varias herramientas concretas de análisis de software basadas en lógica de separación, analizando el tipo de errores que permiten detectar, las clases de programas a los cuales se aplican de manera efectiva, las combinaciones con otras tecnologías de análisis, y las principales limitaciones de las mismas.

  • Título: Síntesis de Sistemas Tolerantes a Fallas
    Expositor: Nicolás Ricci
    Resumen: En esta charla se abordan nociones generales de tolerancia a fallas. Esto se entiende como la posibilidad de un sistema de preservar comportamiento deseable ante situaciones anómalas. Para esto se definen herramientas formales que permiten caracterizar distintos grados de tolerancia. Finalmente se explicará como es posible utilizar estos criterios para atacar el objetivo de construir automáticamente programas que garanticen dichas propiedades de robustez.

  • Título: Compilación certificada sobre máquinas abstractas
    Expositor: Leonardo Rodríguez
    Resumen: Usualmente, cuando compilamos un programa, confiamos totalmente en el compilador. Es decir, asumimos que el código generado se comportará exactamente como lo indica la semántica de nuestro programa original. Pero, ¿realmente podemos garantizar que eso ocurre?. El área de certificación de compiladores lleva ya varios años de desarrollo, y con creciente interés debido al incremento en el uso de software crítico, que demanda mayores garantías de seguridad y confiabilidad. En esta charla veremos algunos de los métodos utilizados para demostrar la corrección de compiladores. En particular nos enfocaremos en un compilador para el cálculo lambda, donde el código generado se ejecuta sobre una máquina abstracta (un modelo de ejecución idealizado, que nos abstrae de los detalles del hardware real). Presentaré también algunos fragmentos de la formalización de esas pruebas en el asistente de demostración Coq.