====== Charlas de Computación ====== 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. [[ http://www.cs.famaf.unc.edu.ar/dokuwiki/doku.php#charlas_del_primer_cuatrimestre_2006 | charlas del primer cuatrimestre 2006]] **Lunes 11 de Septiembre** ==== Reflexiones sobre la enseñanza de la programación ==== === Javier Blanco e invitados sorpresa === ====== ====== **Lunes 4 de Septiembre** ==== charla informal ==== ====== ====== **Lunes 28 de Agosto** ==== A Characterisation of Meaningful Schedulers for Continuous-Time Markov Decision Processes ==== === Nicolás Wolovick === 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 [[ http://depend.cs.uni-sb.de/index.php?id=164 | Sven Johr ]] (Universität des Saarlandes) ====== ====== **Lunes 25 de Septiembre** ==== Título por confirmar ==== === ponente por confirmar === ====== ====== **Lunes 2 de Octubre** ==== Título por confirmar ==== === ponente por confirmar === ====== ====== **Lunes 9 de Octubre** ==== Título por confirmar ==== === ponente por confirmar === ====== ====== **Lunes 23 de Octubre** ==== Título por confirmar ==== === ponente por confirmar === ====== ====== **Lunes 30 de Octubre** ==== Título por confirmar ==== === ponente por confirmar === ====== ====== **Lunes 6 de Noviembre** ==== Título por confirmar ==== === ponente por confirmar === ====== ====== **Lunes 13 de Noviembre** ==== Título por confirmar ==== === ponente por confirmar === ====== ====== **Lunes 20 de Noviembre** ==== Título por confirmar ==== === ponente por confirmar === ====== charlas del primer cuatrimestre 2006 ====== **Viernes 10 de Marzo** **16h** ====Una Introducción a las Lógicas Híbridas ==== ===Carlos Areces=== 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** ====DynAlloy: Upgrading Alloy with Actions==== === Nazareno Aguirre === (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** ====Transformaciones de gramáticas inducidas==== ===Demetrio Martín Vilela=== 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** ==== Construcción de programas que manejan dinámicamente la memoria ==== === Renato Cherini === 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** ==== (Im)proving Split Binary Semaphores ==== === Damián Barsotti === 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** ==== Desarrollo casi automático de sistemas de análisis textual ==== === Laura Alonso i Alemany === 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 | 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 | http://www.cs.famaf.unc.edu.ar/~pln/Proyectos/MineriaTexto/classimina.pdf]] ====== ====== **Lunes 15 de Mayo** ==== charla informal ==== la primera charla informal de computación! con café y galletitas. ====== ====== **Lunes 22 de Mayo** ==== suspendida ==== se suspende la charla por sesión de la Comisión Asesora de Computación. ====== ====== **Lunes 29 de Mayo** ==== Clustering para inducción de categorías sintácticas ==== === Fernando Balbachan === 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) [[http://personales.ciudad.com.ar/fbalbachan/clustering.ppt|Powerpoint de la charla]] ====== ====== **Lunes 5 de Junio** ==== Generación Automática de Invariantes Lineales ==== === Natalia Bidart === 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** ==== Un proceso para la derivación formal de algoritmos que combina el uso de métodos de derivación y la instanciación de esquemas de algoritmos. ==== === Juan Durán === 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** ==== Bancos de ADN: Data Mining y Gestión ==== === Gabriel Infante López === 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** ==== A Characterisation of Meaningful Schedulers for Continuous-Time Markov Decision Processes ==== === Nicolás Wolovick === 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** ====Una Introducción a las Lógicas Híbridas ==== ===Carlos Areces=== 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** ====DynAlloy: Upgrading Alloy with Actions==== === Nazareno Aguirre === (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** ====Transformaciones de gramáticas inducidas==== ===Demetrio Martín Vilela=== 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** ==== Construcción de programas que manejan dinámicamente la memoria ==== === Renato Cherini === 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** ==== (Im)proving Split Binary Semaphores ==== === Damián Barsotti === 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** ==== Desarrollo casi automático de sistemas de análisis textual ==== === Laura Alonso i Alemany === 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 | 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 | http://www.cs.famaf.unc.edu.ar/~pln/Proyectos/MineriaTexto/classimina.pdf]] ====== ====== **Lunes 15 de Mayo** ==== charla informal ==== la primera charla informal de computación! con café y galletitas. ====== ====== **Lunes 22 de Mayo** ==== suspendida ==== se suspende la charla por sesión de la Comisión Asesora de Computación. ====== ====== **Lunes 29 de Mayo** ==== Clustering para inducción de categorías sintácticas ==== === Fernando Balbachan === 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) [[http://personales.ciudad.com.ar/fbalbachan/clustering.ppt|Powerpoint de la charla]] ====== ====== **Lunes 5 de Junio** ==== Generación Automática de Invariantes Lineales ==== === Natalia Bidart === 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** ==== Un proceso para la derivación formal de algoritmos que combina el uso de métodos de derivación y la instanciación de esquemas de algoritmos. ==== === Juan Durán === 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** ==== Bancos de ADN: Data Mining y Gestión ==== === Gabriel Infante López === 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. ====== ======