Registro:
| Documento: | Tesis de Grado |
| Título: | Liquid types para la verificación de smart contracts |
| Autor: | Consoli, Gonzalo |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Fecha de defensa: | 2025-09-24 |
| Fecha en portada: | 2025 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Melgratti, Hernán Claudio |
| Jurado: | Garbervetsky, Diego; Godoy, Javier Ignacio |
| Idioma: | Español |
| Palabras clave: | CONTRATOS INTELIGENTES; SOLIDITY; BLOCKCHAIN; ANALISIS ESTATICO; TIPOS REFINADOS; LIQUID HASKELL; VERIFICACION DE SOFTWARESMART CONTRACTS; SOLIDITY; BLOCKCHAIN; STATIC ANALYSIS; REFINEMENT TYPES; LIQUID HASKELL; SOFTWARE VERIFICATION |
| Formato: | PDF |
| Handle: |
https://hdl.handle.net/20.500.12110/seminario_nCOM000874_Consoli |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000874_Consoli.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000874_Consoli |
| Ubicación: | COM 000874 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Consoli, Gonzalo. (2025). Liquid types para la verificación de smart contracts. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000874_Consoli |
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.
Abstract:
This work presents a tool for the formal verification of smart contracts written in Solidity. Our approach translates Solidity source code into Haskell, leveraging the require and assert statements to derive refinement types, which naturally encode the contracts’ preconditions and postconditions. These refinement types are then used within the Liquid Haskell framework to perform the verification. We illustrate the tool’s capabilities with examples based on Azure and Rosetta contracts, along with specific adaptations tailored to our framework. Finally, we compare our approach against existing verification tools, including SMTChecker and Slither.
Citación:
---------- APA ----------
Consoli, Gonzalo. (2025). Liquid types para la verificación de smart contracts. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000874_Consoli
---------- CHICAGO ----------
Consoli, Gonzalo. "Liquid types para la verificación de smart contracts". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2025.https://hdl.handle.net/20.500.12110/seminario_nCOM000874_Consoli
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000874_Consoli.pdf
Distrubución geográfica
