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:-0200
TZOFFSETTO:-0300
TZNAME:-03
DTSTART:20180218T020000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0300
TZOFFSETTO:-0200
TZNAME:-02
DTSTART:20181104T030000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0200
TZOFFSETTO:-0300
TZNAME:-03
DTSTART:20190217T020000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20191216T170000
DTEND;TZID=America/Sao_Paulo:20191216T180000
DTSTAMP:20260612T181401
CREATED:20191210T121525Z
LAST-MODIFIED:20191210T121525Z
UID:5614-1576515600-1576519200@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Brian Bokser
DESCRIPTION:Título: Verficación de invariantes en tipos de datos replicados con consistencia mixta\nDirectores: Christian Roldán y Hernán Melgratti\nJurados: Juan Pablo Galeotti y Agustín Martinez Suñé\n\nResumen: \n\nLos sistemas geográficamente distribuidos replican su estado sobre diferentes nodos (llamados también réplicas) con el fin de satisfacer requerimientos no-funcionales como la alta disponibilidad. Sin embargo\, dado que la comunicación entre réplicas es asincrónica\, los usuarios de estos sistemas pueden\, temporalmente\, observar discrepancias en la información debido a que acceden a distintas replicas. Por lo tanto\, razonar sobre la correctitud de sistemas geo-replicados se convierte en una tarea difícil. Es así como hoy en día existe la necesidad de contar con herramientas que nos permitan especificar\, modelar y analizar sistemas geo-replicados. Los tipos de datos replicados han sido propuestos a tal fin. Los tipos de datos replicados son análogos a los tipos de datos abstractos\, pero sus operaciones tienen en cuenta los distintos niveles de consistencia\, es decir\, las anomalías o inconsistencias que el sistema puede aceptar hasta que las réplicas converjan a el mismo estado.\n\nEn esta tesis abordamos el problema de probar invariantes de datos sobre tipos de datos replicados. Como modelo formal de computación de sistemas geo-replicados adoptamos Quelea\, un modelo formal de consistencia mixta\, es decir\, que permite combinar operaciones con diferentes niveles de consistencia. Si bien Quelea está equipado con un lenguaje de contratos que permite razonar sobre la consistencia de las operaciones\, no provee herramientas que permitan escribir y probar invariantes de datos a nivel aplicación. Concretamente\, proponemos una técnica para probar invariantes de datos sobre el framework Quelea. Para ello\, proponemos una semántica operacional alternativa que garantiza una propiedad de consistencia conocida como visibilidad causal. Luego\, presentamos un conjunto de proof-rules que permiten verificar invariantes de datos y finalmente ilustramos como estas proof-rules pueden implementarse en F*\, un lenguaje de programación que descarga pruebas sobre un SMT solver.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-brian-bokser/
LOCATION:Laboratorio Turing
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR