Ciencias de la Computación FAMAF

Esta página es de solo lectura. Puedes ver la fuente pero no puedes cambiarla. Pregunta a tu administrador si crees que esto es incorrecto.
====== 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 ﬁre-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 inﬁnite 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 ﬁnally show that each probability measure on the sigma-algebra
of inﬁnite 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 ﬁre-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 inﬁnite 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 ﬁnally show that each probability measure on the sigma-algebra
of inﬁnite 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.

====== ======