Título: Generador de abstracciones para Smart Contracts

Director: Sebastián Uchitel

Co-director: Javier Godoy

Jurados: Dr. Ariel Waissbein y Dr. Victor Braberman

Resumen:

Vamos a abordar la problemática de validar y verificar la corrección de los contratos inteligentes, programas que se ejecutan en una blockchain y pueden manejar recursos de alto valor. Debido a la falta de especificaciones claras del comportamiento esperado y al entorno de ejecución concurrente en el que funcionan, validar la corrección de estos contratos es una tarea compleja. Una manera de facilitar la comprensión del comportamiento de los contratos es construyendo máquinas de estado, pero esta técnica se realiza de manera manual y requiere la traducción del código a un lenguaje de modelado. Por lo tanto, se propone desarrollar una herramienta capaz de construir automáticamente abstracciones para contratos inteligentes para la red Ethereum utilizando ideas similares a las de un estudio anterior y utilizando un analizador estático de programas Solidity. Para esto, se utilizará VeriSol, una herramienta de análisis estático desarrollada por Microsoft Research que verifica la correctitud de las aserciones en un contrato dado.