Experiencia de estudiantes y egresados de LCC que actualmente firmaron un acuerdo con el "Vivero de empresas de Base Tecnológica" para incubar su empresa.

En esta charla presentaremos al grupo de Métodos Formales del Instituto de Computación de la Facultad de Ingenería de la Universidad de la República, Uruguay. En especial haremos énfasis en las actividades y proyectos en curso, en los cursos de grado y postgrado que venimos desarrollando y, en algunas líneas de investigación en las cuales estamos interesados en trabajar en los próximos años.
Presentación

Comentaré la idea general del algoritmo, algunos detalles interesantes y los problemas con los que me encontré durante el estudio y la implementación del algoritmo. El algoritmo ADIOS (Automatic Distillation of Structure), desarrollado por Z. Solan et al., utiliza conceptos de grafos y estadística para detectar patrones en información no estructurada, permitiendo detectar parte de la gramática subyacente y se puede aplicar tanto para lenguajes naturales como para secuencias de ADN.
Presentación)

Se realizará una introducción al Modelo de Madurez de Capacidades Integrado (Capability Maturity Model Integration - CMMI) que es reconocido y adoptado mundialmente en la industria del software como guía para incrementar la productividad y la calidad. El modelo está estructurado en niveles de madurez creciente que contienen áreas de procesos con objetivos y prácticas específicas que la organización debe realizar para producir software bajo cierto nivel de madurez. Dentro de América Latina, nuestro país ha sido el que mayor crecimiento presenta en este campo, superando incluso a algunos países de la Comunidad Europea.
Presentación

Los mecanismos técnicos de restricción al acceso y copia de obras publicadas en formatos digitales nos llevarán a un mundo donde solo tendrán acceso a la información quienes puedan pagarla.
Presentación

La progresiva miniaturización de los chips de computadoras se está acercado al limite de las leyes físicas clásicas. La computación actual busca nuevos caminos y la computación cuántica se presenta como una alternativa diferente y revolucionaria. En esta charla se hará una breve introducción al tema, explicando algunos conceptos básicos, como la noción de qubit, enredo cuántico y paralelismo. Como agregado, se presentará un protocolo inviolable para la transmision de claves a través de canales inseguros.
Presentación

La técnica de semáforos binarios divididos (SBS) brinda tanto los programas que implementan secciones críticas condicionales como los invariantes iniciales que aseguran su corrección. Aplicando la técnica a casos particulares se encuentran programas que admiten simplificaciones.

Este trabajo se concentra en el desarrollo de un procedimiento para verificar la corrección de estas simplificaciones de forma automática. Nos enfocamos particularmente en la eliminación de guardas en las sentencias condicionales finales de los programas, pero el procedimiento encontrado permite su generalización a otros tipos de simplificaciones.

El procedimiento consiste en hacer una búsqueda de nuevos invariantes que avalen la corrección de las simplificaciones. Su implementación fue realizada en ML usando los demostradores Isabelle/HOL y CVC~Lite para demostrar las implicaciones y simplificar fórmulas lógicas.
Presentación

En esta charla daré un breve pantallazo de las principales características de los sistemas de tipos estáticos, sus formas de presentación y el impacto de estas técnicas en desarrollos modernos. Ejemplificaré algunas de las nociones con un lenguaje muy sencillo, intentando mantener el nivel técnico de la charla en un nivel razonable para el público general.
Presentación

En esta charla presentamos el problema de la verificación de modelos aplicada a la verificación de sistemas informáticos. El planteo general del problema es el siguiente:
- dado un sistema S y una propiedad p, averiguar si S satisface p.
La presentación matemática del problema plantea que el sistema informático es una estructura, y la propiedad una fórmula. Por lo tanto, el problema se reduce al de averiguar si p vale en S. Este enfoque proporciona una gran cantidad de variantes, centradas en las siguientes preguntas:
- ¿cómo especificar el sistema?
- ¿cómo especificar sus propiedades?
En esta charla mostraremos algunas de estas variantes que han sido exploradas en el curso de Verificación y Lógica. El curso Modelos y verificación de sistemas de tiempo real realiza una presentación de estas estrategias para el caso específico en que el tiempo se convierte en un actor principal de los sistemas.