Diferencias

Muestra las diferencias entre dos versiones de la página.

--- seminarios_de_metodos_formales:2010 [2010/09/16 13:29] – charla de felipe mpagano
+++ seminarios_de_metodos_formales:2010 [2025/11/15 13:47] (actual) – editor externo 127.0.0.1
@@ Línea 1: / Línea 1: @@
 ====== CAChe! 2010 ======
+**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.
+[[http://vimeo.com/16428540|Video de la charla]] {{:seminarios_de_metodos_formales:franco-luque:slides.pdf|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.
+[[http://vimeo.com/15742631 |Video de la charla]]
+{{:seminarios_de_metodos_formales:raul-fervari:slides.pdf|Presentación}}
 **Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations**
@@ Línea 5: / Línea 39: @@
 Expositor: Felipe Manzano
-Lunes 13 de Septiembre, 14 hs.
+Lunes 13 de Septiembre de 2009, 14 hs.
 We develop an extension of standard symbolic execution to tackle the
@@ Línea 30: / Línea 64: @@
 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.