Ciencias de la Computación FAMAF

• Expositor: Lic. Matias Lee

• Título: Secure Interface Automata.

• Resumen:

Una interface describe cómo un sistema interactua con su entorno. Por esta razón, ellas juegan un papel muy importante en el desarrollo basado en componentes. Dadas las interfaces de 2 componentes sería muy util poder analizar si ellas son compatibles, es decir, si trabajan bien en forma conjunta. En esta charla presentamos un nuevo tipo de interface: Secure Interface Automata. Las mismas nos permiten hablar de “No Interferencia”, una propiedad de seguridad bastante estudiada. Analizamos como se comporta esta propiedad con respecto a la composición. Finalmente, definimos un algoritmo para restringir el comportamiento de una interfaz para obtener la propiedad deseada.

• Expositor: Dr. Nazareno Aguirre

• Título: Descripcion y Analisis de Especificaciones Tabulares de Requisitos usando DynAlloy (trabajo realizado en conjunto con Marcelo Frias, Mariano Moscato, Tom Maibaum y Alan Wassyng)

• Resumen:

En esta charla presentare un lenguaje para la especificacion formal de requisitos llamado SCR (Software Cost Reduction), desarrollado por el Instituto de Investigacion Naval de EEUU. El lenguaje esta fuertemente basado en una notacion tabular, que permite organizar formulas (que describen la relacion que el sistema debe mantener con el ambiente) de manera concisa y clara. El lenguaje posee ademas maduras herramientas de analisis basadas en model checking y demostracion semi-automatica de teoremas.

Discutire ademas algunas limitaciones de SCR, en particular en lo concerniente a la combinacion de tablas. Mostrare como este problema puede atacarse utilizando DynAlloy, una extension al lenguaje de especificaciones Alloy que incorpora acciones (y programas). DynAlloy posee una herramienta de analisis, que indirectamente utiliza SAT solvers mediante la traduccion de especificaciones DynAlloy a Alloy, y el uso del Alloy Analyzer (la herramienta asociada al lenguaje Alloy).

• Expositor: Lic. Araceli Acosta.

• Título: Tolerancia a fallas con NuSMV.

• Resumen:

En esta charla se presentará una extensión al lenguaje NuSMV para especificación de sistemas tolerantes a fallas. Con este nuevo lenguaje queremos contribuir al diseño de una herramienta de model checking que permita verificar propiedades sobre este tipo de sistemas.

• Expositor: Dr. Javier Blanco.

• Título: …

• Resumen: …

• Expositor: Lic. Sergio Giro (http://www.cs.famaf.unc.edu.ar/~sgiro/)

• Titulo: Sobre el poder expresivo de distintas clases de schedulers distribuidos. Parte I

• Resumen:

De acuerdo a trabajos recientes en el área de Sistemas Estocásticos Distribuidos, los schedulers distribuidos son necesarios para obtener resultados realistas durante el análisis. En este trabajo, nuestro objetivo es establecer relaciones entre diferentes clases de schedulers distribuidos. Estas relaciones permiten obtener resultados como, por ejemplo, la complejidad del problema de model-checking para una determinada clase. Mostraremos resultados de NP-hardness e indecidibilidad obtenidos a partir de las relaciones entre clases.

• Expositor: Dr. Pedro R. D'Argenio.

• Titulo: PROCESOS DE MARKOV ETIQUETADOS NO DETERMINISTAS Y TEORÍA DE CONJUNTOS DESCRIPTIVA.

• Resumen:

Los procesos de Markov sobre espacios continuo o con evolución continua del tiempo ocurren naturalmente en sistemas físicos, biológicos, económicos o computacionales. Un trabajo prominente en el área es el desarrollado sobre los denominados procesos de Markov etiquetados (LMP). Los LMP son procesos de decisión de Markov donde cada transición puede distinguirse en cada estado a través de una etiqueta.

El no-determinismo es un aspecto fundamental en computación para la representación abstracta de sistemas. En el marco de este trabajo extendemos los LMP con no-determinismo (las transiciones ya no pueden distinguirse a través de etiquetas) y analizamos un relación de equivalencia sobre estos modelos; la denominada bisimulación.

La definición y el estudio de estos objetos continuos hace necesario el uso de la Teoría de Conjuntos Descriptiva, cuyos resultados típicos incluyen la caracterización de distintas clases de espacios medibles, espacios de medida y determinación de la ``complejidad“ de subconjuntos de espacios métricos (puntos de continuidad y convergencia, etc.)

• Expositor: Lic. Sergio Giro (http://www.cs.famaf.unc.edu.ar/~sgiro/)

• Titulo: Sobre el poder expresivo de distintas clases de schedulers distribuidos. Parte II - final.

• Resumen:

De acuerdo a trabajos recientes en el área de Sistemas Estocásticos Distribuidos, los schedulers distribuidos son necesarios para obtener resultados realistas durante el análisis. En este trabajo, nuestro objetivo es establecer relaciones entre diferentes clases de schedulers distribuidos. Estas relaciones permiten obtener resultados como, por ejemplo, la complejidad del problema de model-checking para una determinada clase. Mostraremos resultados de NP-hardness e indecidibilidad obtenidos a partir de las relaciones entre clases.

• Expositor: Lic. Juan Durán.

• Título: “Algunas consideraciones filosóficas acerca de las Simulaciones Computacionales”

• Resumen:

“El uso de simulaciones computacionales en ciencia es una práctica extremadamente fructífera, no sólo por razones económicas, sino porque la rapidez y precisión para el cálculo producen resultados muy alentadores, inclusive frente a experimentos tradicionales. El estudio filosófico de estos métodos de sustitución de experimentos pretende evaluar estas prácticas a la luz del poder epistémico que de ellas surgen, esto es, discutir las bases mismas de las simulaciones computacionales intentando penetrar en la justificación de la confianza en los resultados. La propuesta es, pues, aproximarse filosóficamente a las simulaciones computacionales mediante la discusión de algunas preguntas tradicionales de corte epistemológico, ontológico y metodológico.”

• Expositor: Dr. Pedro Sanchez Terraf.

• Título: Teoría de Preservación.

• Resumen:

La Teoría de Preservación tuvo su origen en un resultado de G. Birkhoff que caracteriza de una manera algebraica las variedades (clases de álgebras axiomatizables por ecuaciones): una clase K de álgebras es una variedad si y sólo sí es cerrada por las operaciones H, S y P (tomar imágenes homomórficas, subálgebras y construir productos directos, respectivamente). Estos resultados se desarrollaron luego y se pudo caracterizar sintácticamente las fórmulas preservadas por cada una de estos operadores de clase (ahora por separado) y por otras construcciones algebraicas típicas: los productos reducidos y ultraproductos (J. Loś), cadenas de modelos (A. Tarski y R. Vaught) y modelos saturados y especiales (M. Morley y R. Vaught, C.C.Chang y H.J. Keisler), intersecciones de modelos, factores directos, etcétera.

La utilidad de estos resultados es doble: permiten conocer de manera inmediata las propiedades de clausura de una clase de estructuras si tenemos axiomas con una buena sintaxis, y permiten mejorar estos últimos si son conociedas las propiedades de clausura.

• Expositora: Prof. Leticia Losano.

• Título: Aprender a programar en el primer año de la carrera de Ciencias de la Computación. Un análisis basado en las Comunidades de Práctica.

• Resumen:

El objetivo de esta charla es presentar un análisis preliminar de las experiencias y vivencias de estudiantes que ingresan a la universidad para cursar la carrera de Ciencias de la Computación en la Facultad de Matemática, Astronomía y Física de la Universidad Nacional de Córdoba. En el primer año de esta carrera el nivel de deserción y fracaso es elevado. El interés de esta presentación, que comenta parte una investigación en curso, es observar, caracterizar y analizar cómo se realiza el encuentro entre los alumnos recién llegados y la comunidad de la facultad a la que los estudiantes pretenden integrarse.

Durante el primer año de la carrera los estudiantes deben cursar materias introductorias de programación. Esta tarea es abordada desde una perspectiva formal, los programas son vistos como \emph{fórmulas matemáticas largas} las cuales se construyen y demuestran utilizando la inducción matemática. En síntesis, los alumnos deben aprender una nueva notación, un lenguaje de axiomas y reglas de construcción y el significado de demostrar una proposición -por inducción, reducción al absurdo, análisis de casos, contraejemplo-. Simultáneamente, los estudiantes comienzan a vivenciar la presencia de valores y convenciones sociales que sostiene la comunidad. Estas normas implícitas están relacionadas con las características que debe reunir un alumno exitoso, el comportamiento y las actitudes que deben adoptarse, el status de los conocimientos previos del alumno y las relaciones de poder entre profesores y alumnos.

Este complejo y difícil proceso de ingreso a la comunidad involucra la creación, modificación y renegociación del lenguaje, los valores y los conocimientos previos de los aprendices. El éxito en este proceso de iniciación permitirá a los estudiantes lograr una participación cada vez mayor en la comunidad.

A través de una metodología de investigación cualitativa, basada en entrevistas y observaciones de clases se intenta delinear cómo las características de las prácticas áulicas organizan y constituyen el aprendizaje. También se analiza cómo se construyen, de manera situada dentro del aula, las nociones de demostración, abstracción y formalización, consideradas centrales para lograr una participación legítima en la comunidad.

• Expositora: Lic. Natalia Colussi.

• Título: “Derivación Estructurada y uso de Cuantificadores” -

• Resumen:

La derivación estructurada se proponen como una metodología de prueba alternativa a la derivación ecuacional de Dijkstra, extendiendo a esta última con subderivaciones, las cuales permiten que las inferencias se presenten en distintos niveles de detalle, y que el desarrollo de la prueba se lleve a cabo de una manera bastante natural e intuitiva. Esto último hace que el formalismo sea conveniente para la enseñanza en los cursos introductorios de métodos formales, donde los estudiantes deben elaborar ampliamente pruebas formales que garanticen que la construcción del programa respecto de la especificación dada es correcta.

Se presentará una extensión del formalismo estructurado para manejar pruebas que involucran el uso de cuantificadores, donde la notación empleada para describir una cuantificación corresponderá a la notación de lineal de Dijkstra.

También se analizarán algunos de los resultados existentes en la puesta a prueba de este formalismo en distintos niveles de enseñanza.

• Expositor: Lic. Miguel Andres.

• Título: Significant Diagnostic Counterexamples on Probabilistic Model Checking.

• Resumen:

This paper presents a novel technique for counterexample generation in probabilistic model checking of Markov chains and Markov Decision Processes. (Finite) paths in counterexamples are grouped together in witnesses that are likely to provide similar debugging information to the user. We list five properties that witnesses should satisfy in order to be useful as debugging aid: similarity, accuracy, originality, significance, and finiteness. Our witnesses contain paths that behave similarly outside strongly connected components.

Then, we show how to compute these witnesses by reducing the problem of generating counterexamples for general properties over Markov Decision Processes, in several steps, to the easy problem of generating counterexamples for reachability properties over acyclic Markov chains.

• Expositor: Lic. Gustavo Petri.

• Título: Relaxed Memory Models: an Operational Approach POPL'09

• Resumen:

Memory models define an interface between programs written in some language and their implementation, determining which behaviour the memory (and thus a program) is allowed to have in a given model. A minimal guarantee memory models should provide to the programmer is that well-synchronized, that is, data-race free code has a standard semantics. Traditionally, memory models are defined axiomatically, setting constraints on the order in which memory operations are allowed to occur, and the programming language semantics is implicit as determining some of these constraints. In this work we propose a new approach to formalizing a memory model in which the model itself is part of a weak operational semantics for a (possibly concurrent) programming language. We formalize in this way a model that allows write operations to the store to be buffered. This enables us to derive the ordering constraints from the weak semantics of programs, and to prove, at the programming language level, that the weak semantics implements the usual interleaving semantics for data-race free programs, hence in particular that it implements the usual semantics for sequential code.