Termination and Cost Analysis with COSTA and its User Interfaces. - Elvira Albert; Puri Arenas; Samir Genaim; Miguel Gómez-Zamalloa; German Puebla; Diana V. Ramírez-Deantes; Guillermo Román-Díez; Damiano Zanardini (PROLE, 2009)

Verified resource guarantees using COSTA and KeY. - Elvira Albert; Richard Bubel; Samir Genaim; Reiner Hähnle; Germán Puebla; Guillermo Román-Díez (PEPM, 2011)

Verified Resource Guarantees for Heap Manipulating Programs. - Elvira Albert; Richard Bubel; Samir Genaim; Reiner Hähnle; Guillermo Román-Díez (FASE, 2012)

Automatic Inference of Bounds on Resource Consumption. - Elvira Albert; Diego Esteban Alonso-Blas; Puri Arenas; Jesús Correas; Antonio Flores-Montoya; Samir Genaim; Miguel Gómez-Zamalloa; Abu Naser Masud; German Puebla; José Miguel Rojas; Guillermo Román-Díez; Damiano Zanardini (FMCO, 2012)

Incremental resource usage analysis. - Elvira Albert; Jesús Correas; Germán Puebla; Guillermo Román-Díez (PEPM, 2012)

Advanced Topics in Resource Analysis: Certification, Incrementality, Concurrency and Array-Sensitivity. - Guillermo Román-Díez (2012)

Quantified Abstractions of Distributed Systems. - Elvira Albert; Jesús Correas; Germán Puebla; Guillermo Román-Díez (IFM, 2013)

Static Inference of Transmission Data Sizes in Distributed Systems. - Elvira Albert; Jesús Correas Fernández; Enrique Martin-Martin; Guillermo Román-Díez (ISoLA (2), 2014)

Peak Cost Analysis of Distributed Systems. - Elvira Albert; Jesús Correas Fernández; Guillermo Román-Díez (SAS, 2014)

SACO: Static Analyzer for Concurrent Objects. - Elvira Albert; Puri Arenas; Antonio Flores-Montoya; Samir Genaim; Miguel Gómez-Zamalloa; Enrique Martin-Martin; German Puebla; Guillermo Román-Díez (TACAS, 2014)

Conditional termination of loops over heap-allocated data. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Guillermo Román-Díez (Sci. Comput. Program., 2014)

Resource Analysis: From Sequential to Concurrent and Distributed Programs. - Elvira Albert; Puri Arenas; Jesús Correas; Samir Genaim; Miguel Gómez-Zamalloa; Enrique Martin-Martin; Germán Puebla; Guillermo Román-Díez (FM, 2015)

Parallel Cost Analysis of Distributed Systems. - Elvira Albert; Jesús Correas; Einar Broch Johnsen; Guillermo Román-Díez (SAS, 2015)

Non-cumulative Resource Analysis. - Elvira Albert; Jesús Correas Fernández; Guillermo Román-Díez (TACAS, 2015)

Quantified abstract configurations of distributed systems. - Elvira Albert; Jesús Correas Fernández; Germán Puebla; Guillermo Román-Díez (Formal Aspects Comput., 2015)

Object-sensitive cost analysis for concurrent objects. - Elvira Albert; Puri Arenas; Jesús Correas Fernández; Samir Genaim; Miguel Gómez-Zamalloa; Germán Puebla; Guillermo Román-Díez (Softw. Test. Verification Reliab., 2015)

A multi-domain incremental analysis engine and its application to incremental resource analysis. - Elvira Albert; Jesús Correas Fernández; Germán Puebla; Guillermo Román-Díez (Theor. Comput. Sci., 2015)

Resource Analysis of Distributed Systems. - Elvira Albert; Jesús Correas; Guillermo Román-Díez (Theory and Practice of Formal Methods, 2016)

A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY. - Elvira Albert; Richard Bubel; Samir Genaim; Reiner Hähnle; Germán Puebla; Guillermo Román-Díez (Softw. Syst. Model., 2016)

SICOMORo-CM: Development of Trustworthy Systems via Models and Advanced Tools. - Elvira Albert; Pablo C. Cañizares; Esther Guerra; Juan de Lara; Esperanza Marcos; Manuel Núñez 001; Guillermo Román-Díez; Juan Manuel Vara; Damiano Zanardini (STAF Workshops, 2017)

Parallel Cost Analysis. - Elvira Albert; Jesús Correas; Einar Broch Johnsen; Violet Ka I Pun; Guillermo Román-Díez (ACM Trans. Comput. Log., 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)

Time analysis of actor programs. - Cosimo Laneve; Michael Lienhardt; Ka I Pun; Guillermo Román-Díez (J. Log. Algebraic Methods Program., 2019)

Peak resource analysis of concurrent distributed systems. - Elvira Albert; Jesús Correas; Guillermo Román-Díez (J. Syst. Softw., 2019)

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)

When COSTA Met KeY: Verified Cost Bounds. - Elvira Albert; Samir Genaim; Alicia Merayo; Guillermo Román-Díez (The Logic of Software. A Tasting Menu of Formal Methods, 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)

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)

EasyRpl: A web-based tool for modelling and analysis of cross-organisational workflows. - Muhammad Rizwan Ali; Violet Ka I Pun; Guillermo Román-Díez (CoRR, 2025)