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:20250101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20260624T180000
DTEND;TZID=America/Sao_Paulo:20260624T190000
DTSTAMP:20260624T014331
CREATED:20260616T125847Z
LAST-MODIFIED:20260616T125847Z
UID:10671-1782324000-1782327600@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Tomás Chimenti
DESCRIPTION:Título: Abstraktor: Generación automática de abstracciones de protocolo mediante instrumentación de código para fuzzing de sistemas distribuidos \nDirectores: Sebastián Uchitel y Víctor Braberman\nJurados: Prof. Diego Garbervetsky\, Prof. Hernan Melgratti \nResumen: El testing de sistemas distribuidos es un problema de alta complejidad\, donde los bugs más críticos emergen únicamente ante secuencias específicas de fallas. Si bien la especificación formal permite verificar las propiedades lógicas de un protocolo\, garantizar que la implementación concreta en software sea fiel a dicho modelo abstracto continúa siendo un desafío abierto. Esta tesis aborda dicho problema investigando la viabilidad de sintetizar abstracciones generadas dinámicamente a partir de la ejecución real de un sistema para contrastarlas directamente contra una abstracción de la especificación formal. Con este propósito se desarrolló Abstraktor\, una herramienta de instrumentación y análisis que captura variables dinámicas en tiempo de ejecución durante campañas de fuzzing guiadas\, tomando el comportamiento del sistema como una abstracción de predicados. Como caso de estudio\, la técnica se aplicó sobre el motor de almacenamiento distribuido Dqlite\, regido por el protocolo de consenso Raft\, comparando el modelo dinámica resultante contra el modelo de referencia derivado de la especificación formal en TLA+. A diferencia de un método de verificación exhaustiva\, nuestro enfoque utiliza el fuzzing para sondear el espacio de estados y medir la divergencia entre el comportamiento del sistema y el modelo matemático. Los resultados evidencian una aproximación significativa\, pero también revelan discrepancias que categorizamos en dos dimensiones: anomalías funcionales (que pueden ser bugs) y limitaciones de granularidad en la especificación. Esta clasificación no solo mide la conformidad actual\, sino que funciona como un mecanismo de diagnóstico para refinar tanto la fidelidad del modelo como la robustez del código fuente. \nPalabras clave: Sistemas distribuidos\, Abstracción de predicados\, Verificación formal\,TLA+\, Fuzzing\, Raft.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-tomas-chimenti/
LOCATION:Aula 6\, Pab. 1
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR