Registro:
| Documento: | Tesis de Grado |
| Título: | Validación experimental de abstracciones modales para contratos inteligentes |
| Título alternativo: | Experimental validation of modal abstractions for smart contracts |
| Autor: | Incem, Matías Nicolás; Rodríguez, Alejandra Alicia |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Fecha de defensa: | 2025-12-09 |
| Fecha en portada: | 2025 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Garbervetsky, Diego David |
| Jurado: | Brusco, Pablo Daniel; Cristóforis, Pablo Esteban |
| Idioma: | Español |
| Palabras clave: | CONTRATOS INTELIGENTES; BLOCKCHAIN; SOLIDITY; PREDICATE ABSTRACTION; MODAL ABSTRACTION; VERIFICACION FORMAL; ALLOY4PA; ALLOYSMART CONTRACTS; BLOCKCHAIN; SOLIDITY; PREDICATE ABSTRACTION; MODAL ABSTRACTION; FORMAL VERIFICATION; ALLOY4PA; ALLOY |
| Formato: | PDF |
| Handle: |
https://hdl.handle.net/20.500.12110/seminario_nCOM000888_Incem_Rodriguez |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000888_Incem_Rodriguez.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000888_Incem_Rodriguez |
| Ubicación: | COM 000888 |
| 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. Incem, Matías Nicolás; Rodríguez, Alejandra Alicia. (2025). Validación experimental de abstracciones modales para contratos inteligentes. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000888_Incem_Rodriguez |
Resumen:
Los contratos inteligentes (Smart Contracts) son programas que se ejecutan en Blockchain y administran activos de gran valor. Constituyen la base de las finanzas descentralizadas (DeFi), y su carácter inmutable, derivado de la propia Blockchain, implica que un error en su código puede derivar en pérdidas significativas. Esto vuelve esencial su verificación antes del despliegue. Uno de los tipos más frecuentes de errores en los Smart Contracts son los de lógica de negocio. Para analizar este tipo de errores, Predicate Abstractions [1] y Modal Abstractions [2] proponen generar modelos abstractos a partir de contratos escritos en el lenguaje de programación Solidity, enfocándose en la verificación del comportamiento lógico de negocio. Para esto, la herramienta Alloy4PA [3] implementa la propuesta introducida inicialmente en [1] y extendida en [2], utilizando Alloy en entornos Docker y Java. Esta tesis se centra en comprender, reproducir y validar los experimentos descritos en el paper de Modal Abstractions, detallando el proceso de reproducción mediante la herramienta Alloy4PA, y ampliando la evaluación con nuevos casos de estudio que permitan explorar la generalidad y la robustez del enfoque propuesto.
Abstract:
Smart Contracts are programs that run on the Blockchain and manage high-value assets. They form the basis of decentralized finance (DeFi), and their immutable nature, inherited from the Blockchain, means that any error in their code can lead to significant losses. This makes their verification before deployment essential. One of the most common types of errors in Smart Contracts are business logic flaws. To analyze this kind of issue, Predicate Abstractions [1] and Modal Abstractions [2] propose generating abstract models from contracts written in the Solidity programming language, focusing on verifying their logical business behavior. For this purpose, the Alloy4PA tool [3] implements the approach originally introduced in [1] and extended in [2], using the Alloy language within Docker and Java environments. This thesis focuses on understanding, reproducing, and validating the experiments described in the Modal Abstractions paper, detailing the reproduction process using the Alloy4PA tool, and extending the evaluation with new case studies to explore the generality and robustness of the proposed approach.
Citación:
---------- APA ----------
Incem, Matías Nicolás; Rodríguez, Alejandra Alicia. (2025). Validación experimental de abstracciones modales para contratos inteligentes. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000888_Incem_Rodriguez
---------- CHICAGO ----------
Incem, Matías Nicolás; Rodríguez, Alejandra Alicia. "Validación experimental de abstracciones modales para contratos inteligentes". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2025.https://hdl.handle.net/20.500.12110/seminario_nCOM000888_Incem_Rodriguez
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000888_Incem_Rodriguez.pdf
Distrubución geográfica
