reacTIVision: Interfaces de Usuario con Objetos del Mundo Real

Expositor: Franco Luque

Lunes 25 de octubre de 2010, 14 hs.

Resumen: reacTIVision es un framework open source de visión por computadora, que permite el seguimiento a través de una cámara de marcadores fiduciales (“fiducial markers”), un conjunto de símbolos predefinidos que se pueden imprimir y pegar sobre objetos reales. El software reconoce la presencia de múltiples marcadores en la cámara e informa posición, ángulo, velocidad de movimiento y rotación, etc. Esto permite el control de aplicaciones a través de Interfaces de Usuario Tangibles, es decir, manipulando objetos físicos en el mundo real, y en combinación con proyectores permite crear entornos de Realidad Aumentada. reacTIVision también puede reconocer la imagen que forma la presión de dedos sobre superficies transparentes, permitiendo la creación de interfaces Multi-Touch.

El ejemplo más impresionante de uso de reacTIVision es el instrumento de música electrónica Reactable, que ha sido utilizado en vivo por la islandesa Björk, entre otros.

En esta charla/tutorial/demo presentaré la instalación básica del framework, la API de programación y algunos ejemplos muy básicos de uso.

Video de la charla Presentación

Abstraccion por Predicados para Especificaciones DynAlloy

Expositor: Raul Fervari

Lunes 27 de septiembre de 2010, 14 hs.

DynAlloy es una extensión del lenguaje de especificación Alloy, que permite modelar de manera más apropiada propiedades de ejecución de los sistemas de software. DynAlloy provee un soporte completamente automático para la verificación de propiedades de programas, por medio de una busqueda exhaustiva de contraejemplos con dominios acotados. Pero al utilizar mecanismos algorítmicos de verificación, nos encontramos con el problema de la explosión combinatoria de estados, haciendo el análisis imposible para pequeñas cotas. Es por eso, que se presenta un enfoque para lidiar con este problema: Abstracción por Predicados.

La Abstracción por Predicados nos permite incrementar significativamente las cotas de los dominios y de iteraciones en el análisis, y su uso es completamente automático. La implementación de esta técnica es relativamente eficiente, explotando el uso de cálculos previos y realizando la verificación de propiedades bajo demanda sobre la construcción de las trazas abstractas. Además se presentará una técnica de refinamiento de abstracciones para el caso en el que nos encontramos con contraejemplos espúreos, es decir, que violan la propiedad en el modelo abstracto pero que no lo hacen en el concreto. Se presentarán las ideas principales de estos temas, como así también algunos resultados experimentales.

Video de la charla Presentación

Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations

Expositor: Felipe Manzano

Lunes 13 de Septiembre de 2009, 14 hs.

We develop an extension of standard symbolic execution to tackle the analysis of code that uses black box functions like cryptographic primitives. Our extension treats such primitives as symbolic terms that can be rewritten and simplified within an equational theory. Our code runs in a (simplified) LLVM virtual machine. We develop concrete and symbolic semantics for our LLVM, and show our approach sound by proving operational correspondence between the two semantics. We develop a prototype and illustrate the usefulness of our approach with several (sequential code) examples, and discuss next milestones towards symbolically analysing fully concurrent cryptographic protocol implementations.

Video de la charla Presentación

Rule Formats for Non Interference

Expositor: Matias Lee http://www.matiaslee.com.ar

Lunes 17 de Mayo, 17hrs en la Sala Smith (tercer piso)

En un sistema multinivel, usuarios de distintos niveles manejan información con distintos niveles de seguridad. En este contexto, un sistema es seguro si un usuario de bajo nivel no puede interferir en el funcionamiento de un nivel superior u obtener información de este. Esta idea de formaliza con el concepto de non-interferencia. En esta charla presentaremos distintas formalizaciones de ésta. Además, presentaremos formatos de reglas para especificar sistemas de transición que nos garantizan que los sistemas obtenidos satisfacen la propiedad de interés.