Cargando Eventos
Título: Verificación de contratos en Algorand
Director: Diego Garbervetsky
Jurados: Javier Godoy, Esteban Mocskos
Resumen: La creciente adopción de tecnologías blockchain ha generado un interés significativo en la seguridad y confiabilidad de los contratos inteligentes. Algorand, una plataforma blockchain de código abierto, utiliza el lenguaje de script TEAL (Transaction Execution Approval Language) para escribir contratos inteligentes.
La verificación formal de estos contratos es esencial para garantizar su correctitud y prevenir vulnerabilidades. La presente tesis tiene como objetivo desarrollar un enfoque de verificación de TEAL utilizando un acercamiento de traducción a un lenguaje intermedio llamado Boogie, que ha sido utilizado exitosamente para la traducción de varios lenguajes.
El enfoque aplicado se basa en traducir de TEAL a Boogie y la de utilizar la herramienta Corral como verificador, idea similar utilizada en VeriSol para la verificación de contratos inteligentes en Ethereum. Al traducir TEAL a Boogie se podrá utilizar Corral para realizar la verificación formal del código resultante.