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:20240101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20250909T140000
DTEND;TZID=America/Sao_Paulo:20250909T150000
DTSTAMP:20260408T214756
CREATED:20250903T132513Z
LAST-MODIFIED:20250903T132513Z
UID:10163-1757426400-1757430000@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Leo Mansini
DESCRIPTION:Título: Verificación Automática de Smart Contracts Move en Sui\nDirector: Diego Garbervetsky\nJurados: Juan Pablo Galeotti\, Javier Godoy \nResumen\nEn el ecosistema de las blockchains\, la verificación formal de contratos inteligentes es fundamental para garantizar su seguridad y confiabilidad\, evitando vulnerabilidades que podrían resultar en pérdidas económicas o fallas de funcionamiento. Sui\, una blockchain que utiliza el lenguaje Move\, presenta un enfoque innovador para la gestión de objetos y transacciones\, pero aún cuenta con un ecosistema de herramientas de verificación en desarrollo.\nEste trabajo tiene como objetivo explorar métodos para la verificación automática de contratos en Sui. Se realiza un estudio del estado actual de la verificación en Move\, evaluando la herramienta Move Prover en su capacidad para comprobar propiedades de seguridad en módulos escritos para Sui. Además\, se propone un flujo de trabajo alternativo que traduce código Move a Rust de manera controlada\, con el fin de habilitar el uso del verificador Kani\, herramienta enfocada en análisis exhaustivo de propiedades y detección de errores en tiempo de compilación.\nLos resultados muestran que Move Prover no es capaz de interpretar el modelo actual de objetos de Move\, mientras que la traducción a Rust permitió aprovechar verificadores externos con mucha mejor capacidad de verificación\, aunque requirió ajustes manuales y simplificaciones del código para poder representar el funcionamiento de Move en Rust.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-leo-mansini/
LOCATION:Sala 1604
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR