activity
20182023
most citedEthIR: A Framework for High-Level Analysis of Ethereum Bytecode

97 citations · 112 across the 4 of their papers we have counts for

collaborators
Showing cs.PLShow all

6 papers · 1 filter

cs.PL2023

Inferring Needless Write Memory Accesses on Ethereum Bytecode (Extended Version)

Elvira Albert, Jesús Correas, Pablo Gordillo +2

Efficiency is a fundamental property of any type of program, but it is even more so in the context of the programs executing on the blockchain (known as smart contracts). This is b…

cs.PL2020★ 7 cited

Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph

Elvira Albert, Jesús Correas, Pablo Gordillo +2

The EVM language is a simple stack-based language with words of 256 bits, with one significant difference between the EVM and other virtual machine languages (like Java Bytecode or…

cs.PL2019

GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts

Elvira Albert, Jesús Correas, Pablo Gordillo +2

We present the main concepts, components, and usage of GASOL, a Gas AnalysiS and Optimization tooL for Ethereum smart contracts. GASOL offers a wide variety of cost models that all…

cs.PL2019

SAFEVM: A Safety Verifier for Ethereum Smart Contracts

Elvira Albert, Jesús Correas, Pablo Gordillo +2

Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents…

cs.PL2018★ 8 cited

Running on Fumes--Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis

Elvira Albert, Pablo Gordillo, Albert Rubio +1

Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction exec…

cs.PL2018★ 97 cited

EthIR: A Framework for High-Level Analysis of Ethereum Bytecode

Elvira Albert, Pablo Gordillo, Benjamin Livshits +2

Analyzing Ethereum bytecode, rather than the source code from which it was generated, is a necessity when: (1) the source code is not available (e.g., the blockchain only stores th…