May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. - Elvira Albert; Samir Genaim; Pablo Gordillo (SAS, 2015)

May-Happen-in-Parallel Analysis with Returned Futures. - Elvira Albert; Samir Genaim; Pablo Gordillo (ATVA, 2017)

EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. - Elvira Albert; Pablo Gordillo; Benjamin Livshits; Albert Rubio; Ilya Sergey (ATVA, 2018)

GASTAP: A Gas Analyzer for Smart Contracts. - Elvira Albert; Pablo Gordillo; Albert Rubio; Ilya Sergey (CoRR, 2018)

SAFEVM: a safety verifier for Ethereum smart contracts. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (ISSTA, 2019)

Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. - Elvira Albert; Pablo Gordillo; Albert Rubio; Ilya Sergey (VECoS, 2019)

Synthesis of Super-Optimized Smart Contracts Using Max-SMT. - Elvira Albert; Pablo Gordillo; Albert Rubio; Maria Anna Schett (CAV (1), 2020)

Smart, and also Reliable and Gas-Efficient, Contracts. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (ICST, 2020)

GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (TACAS (2), 2020)

Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (CoRR, 2020)

Static Profiling and Optimization of Ethereum Smart Contracts Using Resource Analysis. - Jesús Correas; Pablo Gordillo; Guillermo Román-Díez (IEEE Access, 2021)

Don't run on fumes - Parametric gas bounds for smart contracts. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (J. Syst. Softw., 2021)

Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage". - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Albert Rubio (Zenodo, 2021)

Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage". - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Albert Rubio (Zenodo, 2021)

Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Clara Rodríguez-Núñez; Albert Rubio (IJCAR, 2022)

A Max-SMT Superoptimizer for EVM handling Memory and Storage. - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Albert Rubio (TACAS (1), 2022)

Super-optimization of Smart Contracts. - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Albert Rubio; Maria Anna Schett (ACM Trans. Softw. Eng. Methodol., 2022)

Inferring Needless Write Memory Accesses on Ethereum Bytecode. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (TACAS (1), 2023)

Inferring Needless Write Memory Accesses on Ethereum Bytecode (Extended Version). - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (CoRR, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (ISSTA, 2024)

Neural-guided superoptimization in ethereum. - Matheus Araújo Aguiar; Elvira Albert; Samir Genaim; Pablo Gordillo; Alejandro Hernández-Cerezo; Daniel Kirchner; Albert Rubio (Inf. Softw. Technol., 2025)

Harnessing heap analysis for the synthesis of superoptimized bytecode. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (J. Syst. Softw., 2025)