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 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