todas las charlas tendrán lugar los lunes a las 17h, en la Sala de Computación (3er piso Lado Oeste) excepto si se indica lo contrario.

charlas del primer cuatrimestre 2006

Lunes 11 de Septiembre

Lunes 4 de Septiembre

Lunes 28 de Agosto

Continuous-time Markov decision process are an important vari- ant of labelled transition systems having nondeterminism through labels and stochasticity through exponential fire-time distributions. Nondeterministic choices are resolved using the notion of a scheduler. In this paper we charac- terize the class of measurable schedulers, which is the most general one, and show how a measurable scheduler induces a unique probability measure on the sigma-algebra of infinite paths. We then give evidence that for particu- lar reachability properties it is sufficient to consider a subset of measurable schedulers. Having analyzed schedulers and their induced probability mea- sures we finally show that each probability measure on the sigma-algebra of infinite paths is indeed induced by a measurable scheduler which proves that this class is complete.

trabajo conjunto con Sven Johr (Universität des Saarlandes)

Lunes 25 de Septiembre

Lunes 2 de Octubre

Lunes 9 de Octubre

Lunes 23 de Octubre

Lunes 30 de Octubre

Lunes 6 de Noviembre

Lunes 13 de Noviembre

Lunes 20 de Noviembre

Viernes 10 de Marzo 16h

Las lógicas híbridas son lenguajes modales que incluyen operadores para representar nociones de igualdad y para hacer referencia a elementos del modelo. Recientemente, estos lenguajes recibieron mucha atención, y en la actualidad sus características se conocen en bastante detalle, aunque todavía quedan temas abiertos interesantes.

En esta charla voy a dar una introducción a estos lenguajes que no asume conocimiento previo sobre lenguajes modales, sólo conocimiento estándar sobre lógica clásica.

Viernes 17 de Marzo

(trabajo en conjunto con M. Frias, J. Galeotti y C. Lopez Pombo)

En esta charla, presentaré una extensión al lenguaje de especificaciones formales Alloy, llamada DynAlloy. Esta extensión permite la definición de acciones, y la especificación de aserciones sobre trazas de ejecución de sistemas, siguiendo un estilo similar al de la lógica dinámica. A lo largo de la charla, discutiré sobre los beneficios de adoptar esta versión extendida de Alloy para validar propiedades de sistemas, y mostraré que las especificaciones en DynAlloy pueden, al igual que las especificaciones en Alloy standard, validarse automaticamente. Concluiré con una comparación entre el análisis de especificaciones de ejecuciones en Alloy (mediante una codificación de trazas) y el análisis de especificaciones DynAlloy, mediante un par de casos de estudio.

Lunes 20 de Marzo

Las gramáticas de los lenguajes naturales que se obtienen a partir de lo que la gente efectivamente dice (o más bien, escribe) son redundantes en un sentido que se explicará.

La charla será apta para todo público -aunque ver más adelante-, con una breve introducción a las gramáticas independientes del contexto y a los bancos de árboles.

Lo que tiene de interesante: ¡Nada de ideas verdes desteñidas! ¡Nada de telescopios! Sobre todo, ¡nada de probabilidades!!!

Advertencia: el autor aprovechará la naturaleza paraformal de la charla para usar y abusar de palabras malsonantes y oraciones de múltiples sentidos.

Lunes 27 de Marzo 18h Auditorio de la Facultad

En este trabajo final nos concentramos en la separation logic de Reynolds, y en cómo puede ser utilizada para razonar sobre programas que manejan dinámicamente la memoria.

El objetivo perseguido fue el de ganar experiencia en el cálculo de programas con punteros, desarrollar técnicas para la construcción de los mismos, y de esta manera aproximarse a una metodología que nos permita abordar exitosamente este tipo de programas.

En primer lugar, presentaremos una breve introducción a la lógica, la sintaxis y semántica del lenguaje de comandos y aserciones, y las reglas de inferencia del cálculo. Se mostrará cómo puede utilizarse para definir predicados de abstracción recursivos que nos permitan describir el heap de manera compacta, y faciliten la especificación y construcción de programas que utilizan tipos de datos complejos.

Se introducirá de manera precisa un método para la construcción de programas a partir de una especificación funcional, introducido informalmente en el trabajo de Tamara Rezk. Finalmente veremos un caso de aplicación sobre un problema complejo, que incluye distintos tipos de estructuras de datos compartiendo el mismo espacio de memoria.

Lunes 3 de Abril

It is well-known that binary semaphores can easily ensure mutual exclusion and therefore they can implement critical regions. Moreover, they can be used in a systematic way to implement conditional critical regions through the technique of the split binary semaphore (SBS). This technique provides not only the programs but also some invariants satisfied by the system which ensure the correctness of the solution. The programs so obtained are suitable to be optimised by analysing these invariants and using them to eliminate unnecessary tests.

This work presents a mechanical method to perform these optimisations. The method use the backward propagation technique over a guarded transition system that models the behavior of the programs generated by the SBS technique.

It was implemented integrating the CVC Lite validity checker and Isabelle/Isar theorem prover to our program. The method was tested on a number of examples and the results are reported.

Lunes 17 de Abril

En esta charla describiré un nuevo proyecto del grupo de Procesamiento del Lenguaje Natural: un entorno para la creación casi automática de sistemas de análisis textual, mediante el uso intensivo de técnicas de aprendizaje no supervisado (o minería de datos). Describiré la aproximación general al problema y las soluciones propuestas para cada uno de los tipos de análisis.

más información sobre el proyecto: http://www.cs.famaf.unc.edu.ar/~pln/Proyectos/MineriaTexto/mineria.html

filminas de la charla: http://www.cs.famaf.unc.edu.ar/~pln/Proyectos/MineriaTexto/classimina.pdf

Lunes 15 de Mayo

la primera charla informal de computación! con café y galletitas.

Lunes 22 de Mayo

se suspende la charla por sesión de la Comisión Asesora de Computación.

Lunes 29 de Mayo

Como parte de los modelos estadísticos de aproximación al procesamiento de lenguaje natural, las técnicas de clustering han venido atrayendo la atención convergente de la lingüística computacional y la psicolingüística, como una solución plausible al problema de la adquisición de una gramática a partir de una tabula rasa. La presente investigación se enmarca en dicho paradigma y se propone como uno de los primeros intentos sistemáticos de clustering para grandes corpora que incorpora sustanciales mejoras respecto de trabajos anteriores (Redington et al. 1998). La meta a corto plazo es demostrar empíricamente que la información distribucional es una poderosa herramienta para la inducción de juicios de pertenencia de ítems lexicales a categorías sintácticas. En particular se recurre a una heurística de Decreasing Frequency Profile (Ćavar et al., 2004), información mutua (Shannon, 1948) y al algoritmo K-means (Manning & Schütze, 1999) para una identificación no arbitraria y no apriorística de cues sintácticas que han de sentar las bases del posterior modelado vectorial con clusters de razonable pureza y evidencia de bootstrapping semántico. A más largo plazo se espera sacar provecho de los resultados obtenidos, proponiendo un modelo cognitivo de adquisición de reglas sintácticas refinadas a partir de evidencia translingüística.

Mag. Fernando Balbachan (UBA – Indiana University)

Powerpoint de la charla

Lunes 5 de Junio

En el ámbito de las Ciencias de la Computación, se denomina *invariante* a la propiedad que se mantiene estable en un programa, en un determinado punto del mismo. Una *invariante de programa* es aquella que vale a lo largo de todo el programa. Consecuentemente, el descubrimiento de invariantes es una técnica central en el análisis y verificación de programas secuenciales y de sistemas reactivos.

Dado que el cálculo de invariantes posee una complejidad instrínseca, a lo largo del tiempo ha surgido la necesidad de automatizar ese proceso de cálculo.

Variadas han sido las investigaciones y los resultados al respecto, destacando entre ellos los trabajos de R. Cousot [Cousto78], de N. Shankar [Shankar01], y de Z. Manna [Manna95].

El trabajo final a presentar tiene como objetivo implementar de manera genérica y eficiente el algoritmo propuesto por Cousot en [Cousto78].

Palabras clave:

   1) Poliedros convexos
   2) Programación Lineal
   3) Sistemas de Transiciones
   4) Postcondición más fuerte (SP)
   5) Sistemas Reactivos

Bibliografía:

[Cousot78] Patrick Cousot y Nicolas Halbwachs, “Automatic discovery of linear restraints among variables of a program”, 1978.

[Manna95] Nikolaj Bjorner y Anca Browne y Zohar Manna, “Automatic Generation of Invariants and Assertions”, 1995.

[Shankar01] A. Tiwari y H. Rues and H. Saidi y N. Shankar, “A Technique for Invariant Generation”, 2001.

Lunes 12 de Junio

Dos enfoques bien conocidos para la derivación formal de programas son: el uso de un método de derivación (expresado en términos de técnicas para el diseño y la mejora de eficiencia de algoritmos) y la instanciación de un esquema de algoritmo para una clase de problemas. Ambos enfoques coexisten en lugar de cooperar y tienen distintos tipos de beneficios; por eso, buscamos procesos que combinen ambos enfoques y tengan sus beneficios.

Uno de tales procesos consiste en utilizar un método de derivación para la construcción de un esquema de algoritmo para una clase de problemas, e instanciar ese esquema de algoritmo para la derivación de aplicaciones. Como caso de estudio usamos ese proceso para derivar un esquema de algoritmo que genera un árbol generalizado maximal que satisface una propiedad dada, e instanciamos ese esquema de algoritmo para construir dos ejemplos de aplicación. Basamos nuestro estudio en el álgebra de lenguajes formales y en las álgebras de Kleene.

Lunes 26 de Junio

En esta charla presentaremos un proyecto de desarrollo de software para la gestión y minería de datos sobre los bancos de ADN de la provincia, que se lleva a cabo en esta facultad, financiado por la Agencia Córdoba Ciencia. Describiremos el problema en cuestion, las tecnologia utilizada, los cuestionamientos legales y el estado acutal del proyecto.

Lunes 28 de Agosto

Continuous-time Markov decision process are an important vari- ant of labelled transition systems having nondeterminism through labels and stochasticity through exponential fire-time distributions. Nondeterministic choices are resolved using the notion of a scheduler. In this paper we charac- terize the class of measurable schedulers, which is the most general one, and show how a measurable scheduler induces a unique probability measure on the sigma-algebra of infinite paths. We then give evidence that for particu- lar reachability properties it is sufficient to consider a subset of measurable schedulers. Having analyzed schedulers and their induced probability mea- sures we finally show that each probability measure on the sigma-algebra of infinite paths is indeed induced by a measurable scheduler which proves that this class is complete.

todas las charlas tendrán lugar los lunes a las 17h, en la Sala de Computación (3er piso Lado Oeste) excepto si se indica lo contrario.

Viernes 10 de Marzo 16h

Las lógicas híbridas son lenguajes modales que incluyen operadores para representar nociones de igualdad y para hacer referencia a elementos del modelo. Recientemente, estos lenguajes recibieron mucha atención, y en la actualidad sus características se conocen en bastante detalle, aunque todavía quedan temas abiertos interesantes.

En esta charla voy a dar una introducción a estos lenguajes que no asume conocimiento previo sobre lenguajes modales, sólo conocimiento estándar sobre lógica clásica.

Viernes 17 de Marzo

(trabajo en conjunto con M. Frias, J. Galeotti y C. Lopez Pombo)

En esta charla, presentaré una extensión al lenguaje de especificaciones formales Alloy, llamada DynAlloy. Esta extensión permite la definición de acciones, y la especificación de aserciones sobre trazas de ejecución de sistemas, siguiendo un estilo similar al de la lógica dinámica. A lo largo de la charla, discutiré sobre los beneficios de adoptar esta versión extendida de Alloy para validar propiedades de sistemas, y mostraré que las especificaciones en DynAlloy pueden, al igual que las especificaciones en Alloy standard, validarse automaticamente. Concluiré con una comparación entre el análisis de especificaciones de ejecuciones en Alloy (mediante una codificación de trazas) y el análisis de especificaciones DynAlloy, mediante un par de casos de estudio.

Lunes 20 de Marzo

Las gramáticas de los lenguajes naturales que se obtienen a partir de lo que la gente efectivamente dice (o más bien, escribe) son redundantes en un sentido que se explicará.

La charla será apta para todo público -aunque ver más adelante-, con una breve introducción a las gramáticas independientes del contexto y a los bancos de árboles.

Lo que tiene de interesante: ¡Nada de ideas verdes desteñidas! ¡Nada de telescopios! Sobre todo, ¡nada de probabilidades!!!

Advertencia: el autor aprovechará la naturaleza paraformal de la charla para usar y abusar de palabras malsonantes y oraciones de múltiples sentidos.

Lunes 27 de Marzo 18h Auditorio de la Facultad

En este trabajo final nos concentramos en la separation logic de Reynolds, y en cómo puede ser utilizada para razonar sobre programas que manejan dinámicamente la memoria.

El objetivo perseguido fue el de ganar experiencia en el cálculo de programas con punteros, desarrollar técnicas para la construcción de los mismos, y de esta manera aproximarse a una metodología que nos permita abordar exitosamente este tipo de programas.

En primer lugar, presentaremos una breve introducción a la lógica, la sintaxis y semántica del lenguaje de comandos y aserciones, y las reglas de inferencia del cálculo. Se mostrará cómo puede utilizarse para definir predicados de abstracción recursivos que nos permitan describir el heap de manera compacta, y faciliten la especificación y construcción de programas que utilizan tipos de datos complejos.

Se introducirá de manera precisa un método para la construcción de programas a partir de una especificación funcional, introducido informalmente en el trabajo de Tamara Rezk. Finalmente veremos un caso de aplicación sobre un problema complejo, que incluye distintos tipos de estructuras de datos compartiendo el mismo espacio de memoria.

Lunes 3 de Abril

It is well-known that binary semaphores can easily ensure mutual exclusion and therefore they can implement critical regions. Moreover, they can be used in a systematic way to implement conditional critical regions through the technique of the split binary semaphore (SBS). This technique provides not only the programs but also some invariants satisfied by the system which ensure the correctness of the solution. The programs so obtained are suitable to be optimised by analysing these invariants and using them to eliminate unnecessary tests.

This work presents a mechanical method to perform these optimisations. The method use the backward propagation technique over a guarded transition system that models the behavior of the programs generated by the SBS technique.

It was implemented integrating the CVC Lite validity checker and Isabelle/Isar theorem prover to our program. The method was tested on a number of examples and the results are reported.

Lunes 17 de Abril

En esta charla describiré un nuevo proyecto del grupo de Procesamiento del Lenguaje Natural: un entorno para la creación casi automática de sistemas de análisis textual, mediante el uso intensivo de técnicas de aprendizaje no supervisado (o minería de datos). Describiré la aproximación general al problema y las soluciones propuestas para cada uno de los tipos de análisis.

más información sobre el proyecto: http://www.cs.famaf.unc.edu.ar/~pln/Proyectos/MineriaTexto/mineria.html

filminas de la charla: http://www.cs.famaf.unc.edu.ar/~pln/Proyectos/MineriaTexto/classimina.pdf

Lunes 15 de Mayo

la primera charla informal de computación! con café y galletitas.

Lunes 22 de Mayo

se suspende la charla por sesión de la Comisión Asesora de Computación.

Lunes 29 de Mayo

Como parte de los modelos estadísticos de aproximación al procesamiento de lenguaje natural, las técnicas de clustering han venido atrayendo la atención convergente de la lingüística computacional y la psicolingüística, como una solución plausible al problema de la adquisición de una gramática a partir de una tabula rasa. La presente investigación se enmarca en dicho paradigma y se propone como uno de los primeros intentos sistemáticos de clustering para grandes corpora que incorpora sustanciales mejoras respecto de trabajos anteriores (Redington et al. 1998). La meta a corto plazo es demostrar empíricamente que la información distribucional es una poderosa herramienta para la inducción de juicios de pertenencia de ítems lexicales a categorías sintácticas. En particular se recurre a una heurística de Decreasing Frequency Profile (Ćavar et al., 2004), información mutua (Shannon, 1948) y al algoritmo K-means (Manning & Schütze, 1999) para una identificación no arbitraria y no apriorística de cues sintácticas que han de sentar las bases del posterior modelado vectorial con clusters de razonable pureza y evidencia de bootstrapping semántico. A más largo plazo se espera sacar provecho de los resultados obtenidos, proponiendo un modelo cognitivo de adquisición de reglas sintácticas refinadas a partir de evidencia translingüística.

Mag. Fernando Balbachan (UBA – Indiana University)

Powerpoint de la charla

Lunes 5 de Junio

En el ámbito de las Ciencias de la Computación, se denomina *invariante* a la propiedad que se mantiene estable en un programa, en un determinado punto del mismo. Una *invariante de programa* es aquella que vale a lo largo de todo el programa. Consecuentemente, el descubrimiento de invariantes es una técnica central en el análisis y verificación de programas secuenciales y de sistemas reactivos.

Dado que el cálculo de invariantes posee una complejidad instrínseca, a lo largo del tiempo ha surgido la necesidad de automatizar ese proceso de cálculo.

Variadas han sido las investigaciones y los resultados al respecto, destacando entre ellos los trabajos de R. Cousot [Cousto78], de N. Shankar [Shankar01], y de Z. Manna [Manna95].

El trabajo final a presentar tiene como objetivo implementar de manera genérica y eficiente el algoritmo propuesto por Cousot en [Cousto78].

Palabras clave:

   1) Poliedros convexos
   2) Programación Lineal
   3) Sistemas de Transiciones
   4) Postcondición más fuerte (SP)
   5) Sistemas Reactivos

Bibliografía:

[Cousot78] Patrick Cousot y Nicolas Halbwachs, “Automatic discovery of linear restraints among variables of a program”, 1978.

[Manna95] Nikolaj Bjorner y Anca Browne y Zohar Manna, “Automatic Generation of Invariants and Assertions”, 1995.

[Shankar01] A. Tiwari y H. Rues and H. Saidi y N. Shankar, “A Technique for Invariant Generation”, 2001.

Lunes 12 de Junio

Dos enfoques bien conocidos para la derivación formal de programas son: el uso de un método de derivación (expresado en términos de técnicas para el diseño y la mejora de eficiencia de algoritmos) y la instanciación de un esquema de algoritmo para una clase de problemas. Ambos enfoques coexisten en lugar de cooperar y tienen distintos tipos de beneficios; por eso, buscamos procesos que combinen ambos enfoques y tengan sus beneficios.

Uno de tales procesos consiste en utilizar un método de derivación para la construcción de un esquema de algoritmo para una clase de problemas, e instanciar ese esquema de algoritmo para la derivación de aplicaciones. Como caso de estudio usamos ese proceso para derivar un esquema de algoritmo que genera un árbol generalizado maximal que satisface una propiedad dada, e instanciamos ese esquema de algoritmo para construir dos ejemplos de aplicación. Basamos nuestro estudio en el álgebra de lenguajes formales y en las álgebras de Kleene.

Lunes 26 de Junio

En esta charla presentaremos un proyecto de desarrollo de software para la gestión y minería de datos sobre los bancos de ADN de la provincia, que se lleva a cabo en esta facultad, financiado por la Agencia Córdoba Ciencia. Describiremos el problema en cuestion, las tecnologia utilizada, los cuestionamientos legales y el estado acutal del proyecto.