A Configuration Framework for Distributed Logic Applications. - Jesús Correas Fernández; Francisco Bueno Carrillo (APPIA-GULP-PRODE, 2002)

A Generic Persistence Model for (C)LP Systems. - Jesús Correas; José M. Gómez; Manuel Carro; Daniel Cabeza Gras; Manuel V. Hermenegildo (ICLP, 2003)

A Generic Framework for Context-Sensitive Analysis of Modular Programs. - Germán Puebla; Jesús Correas; Manuel V. Hermenegildo; Francisco Bueno; Maria J. García de la Banda; Kim Marriott; Peter J. Stuckey (Program Development in Computational Logic, 2004)

A Generic Persistence Model for (C)LP Systems (and Two Useful Implementations). - Jesús Correas; José M. Gómez; Manuel Carro; Daniel Cabeza; Manuel V. Hermenegildo (PADL, 2004)

Experiments in Context-Sensitive Analysis of Modular Programs. - Jesús Correas; Germán Puebla; Manuel V. Hermenegildo; Francisco Bueno (LOPSTR, 2005)

Context-Sensitive Multivariant Assertion Checking in Modular Programs. - Pawel Pietrzak; Jesús Correas; Germán Puebla; Manuel V. Hermenegildo (LPAR, 2006)

A practical type analysis for verification of modular prolog programs. - Pawel Pietrzak; Jesús Correas; Germán Puebla; Manuel V. Hermenegildo (PEPM, 2008)

Modular Termination Analysis of Java Bytecode and Its Application to phoneME Core Libraries. - Diana V. Ramírez-Deantes; Jesús Correas; Germán Puebla (FACS, 2010)

Extending the TOY System with the ECLiPSe Solver over Sets of Integers. - Sonia Estévez Martín; Jesús Correas Fernández; Fernando Sáenz-Pérez (FLOPS, 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)

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)

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)

Enhancing set constraint solvers with bound consistency. - Jesús Correas Fernández; Sonia Estévez Martín; Fernando Sáenz-Pérez (Expert Syst. Appl., 2018)

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)

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)

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)