Título: Liquid Types para la verificación de smart contracts
Director: Hernán Melgratti
Jurados: Diego Garbervetsky, Javier Godoy.

Resumen:
En este trabajo se desarrolló una herramienta para la verificación de smart contracts escritos en Solidity. La estrategia empleada consiste en traducir el código fuente de Solidity a Haskell, utilizando las instrucciones require y assert como base para generar refinement types, los cuales se interpretan como precondiciones y postcondiciones. Estos tipos refinados se utilizan posteriormente en el proceso de verificación mediante Liquid Haskell.
Además, se presentan ejemplos de uso con contratos de Azure y Rosetta, así como
adaptaciones específicas para esta herramienta. Finalmente, se incluye una comparación con otras herramientas de verificación existentes, como SMTChecker y Slither.