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

F. B. Schneider (“Understanding protocols for Byzantine clock synchronization”) generalizes a number of protocols for Byzantine fault-tolerant clock synchronization and presents a uniform proof for their correctness. In Schneider's schema, each processor maintains a local clock by periodically adjusting each value to one computed by a convergence function applied to the readings of all the clocks. Then, correctness of an algorithm, i.e. that the readings of two clocks at any time are within a fixed bound of each other, is based upon some conditions on the convergence function. To prove that a particular clock synchronization algorithm is correct it suffices to show that the convergence function used by the algorithm meets Schneider's conditions. Using the theorem prover Isabelle, we formalize the proofs that the convergence functions of two algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch, meet Schneider's conditions. Furthermore, we experiment on handling some parts of the proofs with fully automatic tools like ICS and CVC-lite. This is part of a joint work with Alwen Tiu and Leonor P. Nieto “ Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools” in proceedings of AVOCS 2005.

Lunes 10 de Abril

Lunes 17 de Abril

Lunes 24 de Abril

Lunes 8 de Mayo

Lunes 15 de Mayo

Lunes 29 de Mayo

Lunes 5 de Junio

Lunes 12 de Junio