
BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Departamento de Computación - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Departamento de Computación
X-ORIGINAL-URL:https://www.dc.uba.ar
X-WR-CALDESC:Eventos para Departamento de Computación
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/Sao_Paulo
BEGIN:STANDARD
TZOFFSETFROM:-0300
TZOFFSETTO:-0300
TZNAME:-03
DTSTART:20200101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20210610T110000
DTEND;TZID=America/Sao_Paulo:20210610T110000
DTSTAMP:20260514T205151
CREATED:20210604T164206Z
LAST-MODIFIED:20210604T164206Z
UID:6725-1623322800-1623322800@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Pablo Gómez
DESCRIPTION:Título: Verificación de correctitud para tipos de datos replicados en Coq\nDirectores: Christian Roldán y Hernán Melgratti\nJurados: Fernando Asteasuain y Agustín Martinez Suñé \nResumen: \nLa replicacion de datos es un concepto fundamental en sistemas distribuidos ya que ofrece garantías como escalabilidad y alta disponibilidad a expensas de tener una vision inconsistente del estado del sistema. Esto significa que los usuarios de dicho sistema\, temporalmente\, podrían percibir diferencias sobre el estado del mismo. \nEn particular\, esta tesis se concentra en un enfoque de replicación basada en estados\, donde cada réplica (o nodo) que compone al sistema\, transmite su estado al resto de las réplicas con el fin que estas puedan combinarlo con su propio estado y alcancen así un mismo estado común. La literatura propone los tipos de datos replicados o RDTs (por su acrónimo en inglés\, Replicated Data Types) quienes lidean con inconsistencias temporales que puedan existir y resuelven de forma automática cuando existen conflictos entre escrituras concurrentes. Diferentes líneas de investigación han abordado el problema de especificar e implementar RDTs. Más aún\, hay demostraciones manuales sobre la correcta implementación de un RDT con respecto a su especificación. \nEn esta tesis proponemos abordar el problema de formalizar y verificar la correcta implementación de RDTs utilizando el asistente de demostraciones Coq. Coq es un sistema formal de semidesición de manejo de demostraciones de teoremas chequeadas por computadora. Proveemos por lo tanto\, de un marco de trabajo para verificar la correctitud de RDTs de una manera computarizada\, lo cual ofrece una alternativa confiable y mecánica de abordar esta tarea. Mas concretamente\, en esta tesis nos centramos en realizar la experiencia de formalizar en Coq una especificacion y una implementacion de un RDT (tomando como caso de estudio el tipo de datos: Contador). Para esto\, (i) mostraremos como transformar las definiciones existentes en definiciones equivalentes en Coq. Luego\, (ii) probaremos que la implementacion del tipo de datos es correcta\, basándonos en un resultado  que establece la existencia de una relacion de simulacion entre la semantica operacional asociada a la especificacion\, y la implementacion concreta del Contador. Finalmente\, (iii) presentamos una prueba en el asistente sobre la correcta implementación del tipo de datos\, mostrando para esto\, la existencia de dicha relación de simulación.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-pablo-gomez/
LOCATION:ZOOM
CATEGORIES:Agenda
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20210610T110000
DTEND;TZID=America/Sao_Paulo:20210610T130000
DTSTAMP:20260514T205151
CREATED:20210608T124014Z
LAST-MODIFIED:20210608T124014Z
UID:6731-1623322800-1623330000@www.dc.uba.ar
SUMMARY:Lecciones aprendidas y desafíos pendientes
DESCRIPTION:Los invitamos a la décima charla de la edición 2021 del seminario. Esta vez tenemos el honor de contar con la visita del Dr. Pedro Cahn\, Director Científico de la Fundación Huésped y miembro del equipo asesor del gobierno nacional en temas covid. \nQuién: Dr. Pedro Cahn\, Director Científico de la Fundación Huésped\nCuándo: Jueves 10 de Junio\, 11 hs.\nLink zoom: https://exactas-uba.zoom.us/j/94443673957\nTambién lo podes ver en youtube acá:\nhttps://www.youtube.com/channel/UCzcbeaNQEIhOFBRBdYx1NEA \nTítulo: Lecciones aprendidas y desafíos pendientes \nResumen: Presentaré un resumen del impacto epidemiológico a la fecha\, mecanismos de transmisión\, clínica\, tratamientos disponibles\, vacunas e impacto social de la pandemia. Abriré la discusión sobre virtudes y defectos en las respuestas de nuestro país y el mundo frente a la pandemia. \nPedro Cahn es Médico infectólogo\, Doctor en Medicina UBA. Director Científico\, Fundación Huésped. Ex Jefe de Infectología y actual consultor de la División Infectología\, Htal. Juan Fernandez. Ex Profesor Titular de Infectología\, Facultad de Medicina\, UBA. Asesor externo de OMS\, ONUSIDA\, OPS y Ministerio de Salud\, Argentina. Past-President\, International AIDS Society y autor de más de 200 trabajos publicados en revistas con referato.
URL:https://www.dc.uba.ar/event/lecciones-aprendidas-y-desafios-pendientes/
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR