Polygenetic Partial Evaluation of Lazy Functional Logic Programs. - Elvira Albert; María Alpuente; Moreno Falaschi; Pascual Julián Iranzo; Germán Vidal (APPIA-GULP-PRODE, 1998)

Improving Control in Functional Logic Program Specialization. - Elvira Albert; María Alpuente; Moreno Falaschi; Pascual Julián Iranzo; Germán Vidal (SAS, 1998)

A Partial Evaluation Framework for Curry Programs. - Elvira Albert; María Alpuente; Michael Hanus; Germán Vidal (LPAR, 1999)

Improving Functional Logic Programs by Difference-Lists. - Elvira Albert; César Ferri; Frank Steiner; Germán Vidal (ASIAN, 2000)

Measuring the Effectiveness of Partial Evaluation. - Elvira Albert; Sergio Antoy; Germán Vidal (LOPSTR, 2000)

Measuring the Effectiveness of Partial Evaluation in Functional Logic Languages. - Elvira Albert; Sergio Antoy; Germán Vidal (LOPSTR (LNCS 2042: Selected Papers), 2000)

Using an Abstract Representation to Specialize Functional Logic Programs. - Elvira Albert; Michael Hanus; Germán Vidal (LPAR, 2000)

A Formal Approach to Reasoning about the Effectiveness of Partial Evaluation. - Elvira Albert; Sergio Antoy; Germán Vidal (WFLP, 2000)

List-Processing Optimizations in a Multi-Paradigm Declarative Language. - Elvira Albert; César Ferri; Frank Steiner; Germán Vidal (WFLP, 2000)

Realistic Program Specialization in a Multi-Paradigm Language. - Elvira Albert; Michael Hanus; Germán Vidal (WFLP, 2000)

A Practical Partial Evaluator for a Multi-Paradigm Declarative Language. - Elvira Albert; Michael Hanus; Germán Vidal (FLOPS, 2001)

Symbolic Profiling for Multi-paradigm Declarative Languages. - Elvira Albert; Germán Vidal (LOPSTR, 2001)

Partial evaluation of multi-paradigm declarative languages. - Elvira Albert (AI Commun., 2001)

The Narrowing-driven Approach to Functional Logic Program Specialization. - Elvira Albert; Germán Vidal (New Gener. Comput., 2001)

A Deterministic Operational Semantics for Functional Logic Programs. - Elvira Albert; Michael Hanus; Frank Huch; Javier Oliver 001; Germán Vidal (APPIA-GULP-PRODE, 2002)

An Operational Semantics for Declarative Multi-Paradigm Languages. - Elvira Albert; Michael Hanus; Frank Huch; Javier Oliver 001; Germán Vidal (WRS, 2002)

Operational Semantics for Functional Logic Languages. - Elvira Albert; Michael Hanus; Frank Huch; Javier Oliver 001; Germán Vidal (WFLP, 2002)

A Practical Partial Evaluation Scheme for Multi-Paradigm Declarative Languages. - Elvira Albert; Michael Hanus; Germán Vidal (J. Funct. Log. Program., 2002)

Time Equations for Lazy Functional (Logic) Languages. - Elvira Albert; Josep Silva; Germán Vidal (APPIA-GULP-PRODE, 2003)

A residualizing semantics for the partial evaluation of functional logic programs. - Elvira Albert; Michael Hanus; Germán Vidal (Inf. Process. Lett., 2003)

Some Techniques for Automated, Resource-Aware Distributed and Mobile Computing in a Multi-paradigm Programming System. - Manuel V. Hermenegildo; Elvira Albert; Pedro López-García 001; Germán Puebla (Euro-Par, 2004)

Abstract Interpretation-Based Mobile Code Certification. - Elvira Albert; Germán Puebla; Manuel V. Hermenegildo (ICLP, 2004)

Efficient Local Unfolding with Ancestor Stacks for Full Prolog. - Germán Puebla; Elvira Albert; Manuel V. Hermenegildo (LOPSTR, 2004)

Abstraction-Carrying Code. - Elvira Albert; Germán Puebla; Manuel V. Hermenegildo (LPAR, 2004)

Experiments in abstract interpretation-based code certification for pervasive systems. - Elvira Albert; Germán Puebla; Manuel V. Hermenegildo (SMC (2), 2004)

An Abstract Interpretation-based Approach to Mobile Code Safety. - Elvira Albert; Germán Puebla; Manuel V. Hermenegildo (COCV@ETAPS, 2004)

A Generic Framework for the Analysis and Specialization of Logic Programs. - Germán Puebla; Elvira Albert; Manuel V. Hermenegildo (ICLP, 2005)

Non-leftmost Unfolding in Partial Evaluation of Logic Programs with Impure Predicates. - Elvira Albert; Germán Puebla; John P. Gallagher (LOPSTR, 2005)

Converting One Type-Based Abstract Domain to Another. - John P. Gallagher; Germán Puebla; Elvira Albert (LOPSTR, 2005)

Abstraction carrying code and resource-awareness. - Manuel V. Hermenegildo; Elvira Albert; Pedro López-García 001; Germán Puebla (PPDP, 2005)

Operational semantics for declarative multi-paradigm languages. - Elvira Albert; Michael Hanus; Frank Huch; Javier Oliver 001; Germán Vidal (J. Symb. Comput., 2005)

Reduced Certificates for Abstraction-Carrying Code. - Elvira Albert; Puri Arenas-Sánchez; Germán Puebla; Manuel V. Hermenegildo (ICLP, 2006)

An Incremental Approach to Abstraction-Carrying Code. - Elvira Albert; Puri Arenas; Germán Puebla (LPAR, 2006)

Abstract Interpretation with Specialized Definitions. - Germán Puebla; Elvira Albert; Manuel V. Hermenegildo (SAS, 2006)

Cost Analysis of Java Bytecode. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Damiano Zanardini (ESOP, 2007)

COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. - Elvira Albert; Puri Arenas; Samir Genaim; German Puebla; Damiano Zanardini (FMCO, 2007)

Heap space analysis for java bytecode. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa (ISMM, 2007)

Type-Based Homeomorphic Embedding and Its Applications to Online Partial Evaluation. - Elvira Albert; John P. Gallagher; Miguel Gómez-Zamalloa; Germán Puebla (LOPSTR, 2007)

Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. - Elvira Albert; Miguel Gómez-Zamalloa; Laurent Hubert; Germán Puebla (PADL, 2007)

Some Issues on Incremental Abstraction-Carrying Code - Elvira Albert; Puri Arenas; Germán Puebla (CoRR, 2007)

Experiments in Cost Analysis of Java Bytecode. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Damiano Zanardini (Bytecode@ETAPS, 2007)

Improving the Decompilation of Java Bytecode to Prolog by Partial Evaluation. - Miguel Gómez-Zamalloa; Elvira Albert; Germán Puebla (Bytecode@ETAPS, 2007)

Formal Techniques for Java-Like Programs. - Elvira Albert; Anindya Banerjee 001; Sophia Drossopoulou; Marieke Huisman; Atsushi Igarashi; Gary T. Leavens; Peter Müller 001; Tobias Wrigstad (ECOOP Workshops, 2008)

Termination Analysis of Java Bytecode. - Elvira Albert; Puri Arenas; Michael Codish; Samir Genaim; Germán Puebla; Damiano Zanardini (FMOODS, 2008)

Test Data Generation of Bytecode by CLP Partial Evaluation. - Elvira Albert; Miguel Gómez-Zamalloa; Germán Puebla (LOPSTR, 2008)

Removing useless variables in cost analysis of Java bytecode. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Damiano Zanardini (SAC, 2008)

Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (SAS, 2008)

Modular Decompilation of Low-Level Code by Partial Evaluation. - Miguel Gómez-Zamalloa; Elvira Albert; Germán Puebla (SCAM, 2008)

Cost Relation Systems: A Language-Independent Target Language for Cost Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (PROLE, 2008)

Abstraction-Carrying Code: a Model for Mobile Code Safety. - Elvira Albert; Germán Puebla; Manuel V. Hermenegildo (New Gener. Comput., 2008)

Asymptotic Resource Usage Bounds. - Elvira Albert; Diego Esteban Alonso-Blas; Puri Arenas; Samir Genaim; German Puebla (APLAS, 2009)

Field-Sensitive Value Analysis by Field-Insensitive Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (FM, 2009)

Comparing Cost Functions in Resource Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Israel Herraiz; German Puebla (FOPARA, 2009)

Resource Usage Analysis and Its Application to Resource Certification. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Damiano Zanardini (FOSAD, 2009)

Live heap space analysis for languages with garbage collection. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa (ISMM, 2009)

On the Generation of Test Data for Prolog by Partial Evaluation - Miguel Gómez-Zamalloa; Elvira Albert; Germán Puebla (CoRR, 2009)

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)

Preface. - Elvira Albert; Samir Genaim (BYTECODE@ETAPS, 2009)

Decompilation of Java bytecode to Prolog by partial evaluation. - Miguel Gómez-Zamalloa; Elvira Albert; Germán Puebla (Inf. Softw. Technol., 2009)

Type-based homeomorphic embedding for online termination. - Elvira Albert; John P. Gallagher; Miguel Gómez-Zamalloa; Germán Puebla (Inf. Process. Lett., 2009)

Parametric inference of memory requirements for garbage collected languages. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa (ISMM, 2010)

Compositional CLP-Based Test Data Generation for Imperative Languages. - Elvira Albert; Miguel Gómez-Zamalloa; José Miguel Rojas; Germán Puebla (LOPSTR, 2010)

PET: a partial evaluation-based test case generation tool for Java bytecode. - Elvira Albert; Miguel Gómez-Zamalloa; Germán Puebla (PEPM, 2010)

From Object Fields to Local Variables: A Practical Approach to Field-Sensitive Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; German Puebla; Diana V. Ramírez-Deantes (SAS, 2010)

Test case generation for object-oriented imperative languages in CLP. - Miguel Gómez-Zamalloa; Elvira Albert; Germán Puebla (Theory Pract. Log. Program., 2010)

Cost Analysis of Concurrent OO Programs. - Elvira Albert; Puri Arenas; Samir Genaim; Miguel Gómez-Zamalloa; German Puebla (APLAS, 2011)

Simulating Concurrent Behaviors with Worst-Case Cost Bounds. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa; Einar Broch Johnsen; Rudolf Schlatte; Silvia Lizeth Tapia Tarifa (FM, 2011)

Task-level analysis for a language with async/finish parallelism. - Elvira Albert; Puri Arenas; Samir Genaim; Damiano Zanardini (LCTES, 2011)

Resource-Driven CLP-Based Test Case Generation. - Elvira Albert; Miguel Gómez-Zamalloa; José Miguel Rojas (LOPSTR, 2011)

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)

More Precise Yet Widely Applicable Cost Analysis. - Elvira Albert; Samir Genaim; Abu Naser Masud (VMCAI, 2011)

jPET: An Automatic Test-Case Generator for Java. - Elvira Albert; Israel Cabanas; Antonio Flores-Montoya; Miguel Gómez-Zamalloa; Sergio Gutierrez (WCRE, 2011)

Closed-Form Upper Bounds in Static Cost Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (J. Autom. Reason., 2011)

Efficient local unfolding with ancestor stacks. - Germán Puebla; Elvira Albert; Manuel V. Hermenegildo (Theory Pract. Log. Program., 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)

Automated Extraction of Abstract Behavioural Models from JMS Applications. - Elvira Albert; Bjarte M. Østvold; José Miguel Rojas (FMICS, 2012)

Analysis of May-Happen-in-Parallel in Concurrent Objects. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim (FMOODS/FORTE, 2012)

Towards Testing Concurrent Objects in CLP. - Elvira Albert; Puri Arenas; Miguel Gómez-Zamalloa (ICLP (Technical Communications), 2012)

Automatic Inference of Resource Consumption Bounds. - Elvira Albert; Puri Arenas; Samir Genaim; Miguel Gómez-Zamalloa; Germán Puebla (LPAR, 2012)

Symbolic Execution of Concurrent Objects in CLP. - Elvira Albert; Puri Arenas; Miguel Gómez-Zamalloa (PADL, 2012)

COSTABS: a cost and termination analyzer for ABS. - Elvira Albert; Puri Arenas; Samir Genaim; Miguel Gómez-Zamalloa; Germán Puebla (PEPM, 2012)

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

MayPar: a may-happen-in-parallel analyzer for concurrent objects. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim (SIGSOFT FSE, 2012)

The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. - Peter Y. H. Wong; Elvira Albert; Radu Muschevici; José Proença; Jan Schäfer 002; Rudolf Schlatte (Int. J. Softw. Tools Technol. Transf., 2012)

Cost analysis of object-oriented bytecode programs. - Elvira Albert; Puri Arenas; Samir Genaim; German Puebla; Damiano Zanardini (Theor. Comput. Sci., 2012)

Certificate size reduction in abstraction-carrying code. - Elvira Albert; Puri Arenas; Germán Puebla; Manuel V. Hermenegildo (Theory Pract. Log. Program., 2012)

Termination and Cost Analysis of Loops with Concurrent Interleavings. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim; Enrique Martin-Martin (ATVA, 2013)

May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects. - Antonio Flores-Montoya; Elvira Albert; Samir Genaim (FMOODS/FORTE, 2013)

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

A Transformational Approach to Resource Analysis with Typed-Norms. - Elvira Albert; Samir Genaim; Raúl Gutiérrez (LOPSTR, 2013)

May-Happen-in-Parallel Analysis for Priority-Based Scheduling. - Elvira Albert; Samir Genaim; Enrique Martin-Martin (LPAR, 2013)

Engineering virtualized services. - Elvira Albert; Frank S. de Boer; Reiner Hähnle; Einar Broch Johnsen; Cosimo Laneve (NordiCloud, 2013)

aPET: a test case generation tool for concurrent objects. - Elvira Albert; Puri Arenas; Miguel Gómez-Zamalloa; Peter Y. H. Wong (ESEC/SIGSOFT FSE, 2013)

Heap space analysis for garbage collected languages. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa (Sci. Comput. Program., 2013)

On the Inference of Resource Usage Upper and Lower Bounds. - Elvira Albert; Samir Genaim; Abu Naser Masud (ACM Trans. Comput. Log., 2013)

A CLP heap solver for test case generation. - Elvira Albert; Maria J. García de la Banda; Miguel Gómez-Zamalloa; José Miguel Rojas; Peter J. Stuckey (Theory Pract. Log. Program., 2013)

Actor- and Task-Selection Strategies for Pruning Redundant State-Exploration in Testing. - Elvira Albert; Puri Arenas; Miguel Gómez-Zamalloa (FORTE, 2014)

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)

Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency. - Elvira Albert; Puri Arenas; Miguel Gómez-Zamalloa; José Miguel Rojas (SFM, 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)

Selected and extended papers from Partial Evaluation and Program Manipulation 2013. - Elvira Albert; Shin-Cheng Mu (Sci. Comput. Program., 2014)

Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS. - Elvira Albert; Frank S. de Boer; Reiner Hähnle; Einar Broch Johnsen; Rudolf Schlatte; Silvia Lizeth Tapia Tarifa; Peter Y. H. Wong (Serv. Oriented Comput. Appl., 2014)

Test Case Generation of Actor Systems. - Elvira Albert; Puri Arenas; Miguel Gómez-Zamalloa (ATVA, 2015)

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)

May-Happen-in-Parallel Analysis with Condition Synchronization. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim (FOPARA, 2015)

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

May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. - Elvira Albert; Samir Genaim; Pablo Gordillo (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)

A practical comparator of cost functions and its applications. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (Sci. Comput. Program., 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)

SYCO: a systematic testing tool for concurrent objects. - Elvira Albert; Miguel Gómez-Zamalloa; Miguel Isabel (CC, 2016)

Combining Static Analysis and Testing for Deadlock Detection. - Elvira Albert; Miguel Gómez-Zamalloa; Miguel Isabel (IFM, 2016)

A Formal, Resource Consumption-Preserving Translation of Actors to Haskell. - Elvira Albert; Nikolaos Bezirgiannis; Frank S. de Boer; Enrique Martin-Martin (LOPSTR, 2016)

Testing of concurrent and imperative software using CLP. - Elvira Albert; Puri Arenas; Miguel Gómez-Zamalloa (PPDP, 2016)

Resource-usage-aware configuration in software product lines. - Damiano Zanardini; Elvira Albert; Karina Villela (J. Log. Algebraic Methods Program., 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)

May-Happen-in-Parallel Analysis for Actor-Based Concurrency. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim; Enrique Martin-Martin (ACM Trans. Comput. Log., 2016)

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

Context-Sensitive Dynamic Partial Order Reduction. - Elvira Albert; Puri Arenas; Maria Garcia de la Banda; Miguel Gómez-Zamalloa; Peter J. Stuckey (CAV (1), 2017)

Generation of Initial Contexts for Effective Deadlock Detection. - Elvira Albert; Miguel Gómez-Zamalloa; Miguel Isabel (LOPSTR, 2017)

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)

Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim; Enrique Martin-Martin (J. Autom. Reason., 2017)

Preface for selected and extended papers from Principles and Practice of Declarative Programming (PPDP'15). - Elvira Albert (Sci. Comput. Program., 2017)

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

Constrained Dynamic Partial Order Reduction. - Elvira Albert; Miguel Gómez-Zamalloa; Miguel Isabel; Albert Rubio (CAV (2), 2018)

SDN-Actors: Modeling and Verification of SDN Programs. - Elvira Albert; Miguel Gómez-Zamalloa; Albert Rubio; Matteo Sammartino; Alexandra Silva 001 (FM, 2018)

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

Systematic testing of actor systems. - Elvira Albert; Puri Arenas; Miguel Gómez-Zamalloa (Softw. Test. Verification Reliab., 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)

Optimal context-sensitive dynamic partial order reduction with observers. - Elvira Albert; Maria Garcia de la Banda; Miguel Gómez-Zamalloa; Miguel Isabel; Peter J. Stuckey (ISSTA, 2019)

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)

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

Resource Analysis driven by (Conditional) Termination Proofs. - Elvira Albert; Miquel Bofill; Cristina Borralleras; Enrique Martin-Martin; Albert Rubio (Theory Pract. Log. Program., 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)

Actor-Based Model Checking for SDN Networks. - Elvira Albert; Miguel Gómez-Zamalloa; Miguel Isabel; Albert Rubio; Matteo Sammartino; Alexandra Silva 001 (CoRR, 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)

A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell. - Elvira Albert; Nikolaos Bezirgiannis; Frank S. de Boer; Enrique Martin-Martin (Fundam. Informaticae, 2020)

Taming callbacks for smart contract modularity. - Elvira Albert; Shelly Grossman; Noam Rinetzky; Clara Rodríguez-Núñez; Albert Rubio; Mooly Sagiv (Proc. ACM Program. Lang., 2020)

A Transformational Approach to Resource Analysis with Typed-norms Inference. - Elvira Albert; Samir Genaim; Raúl Gutiérrez; Enrique Martin-Martin (Theory Pract. Log. Program., 2020)

Lower-Bound Synthesis Using Loop Specialization and Max-SMT. - Elvira Albert; Samir Genaim; Enrique Martin-Martin; Alicia Merayo; Albert Rubio (CAV (2), 2021)

Certified Abstract Cost Analysis. - Elvira Albert; Reiner Hähnle; Alicia Merayo; Dominic Steinhöfel (FASE, 2021)

Actor-based model checking for Software-Defined Networks. - Elvira Albert; Miguel Gómez-Zamalloa; Miguel Isabel; Albert Rubio; Matteo Sammartino; Alexandra Silva 001 (J. Log. Algebraic Methods Program., 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)

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)

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)

Distilling Constraints in Zero-Knowledge Protocols. - Elvira Albert; Marta Bellés-Muñoz; Miguel Isabel; Clara Rodríguez-Núñez; Albert Rubio (CAV (1), 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)

Artifact of the Paper "Formally Verified EVM Block-Optimizations". - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (Zenodo, 2022)

Formally Verified EVM Block-Optimizations. - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (CAV (3), 2023)

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)

Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. - Elvira Albert; Shelly Grossman; Noam Rinetzky; Clara Rodríguez-Núñez; Albert Rubio; Mooly Sagiv (IEEE Trans. Dependable Secur. Comput., 2023)

Artifact of the Paper "Formally Verified EVM Block-Optimizations". - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (Zenodo, 2023)

Artifact of the Paper "Formally Verified EVM Block-Optimizations". - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (Zenodo, 2023)

Optimal dynamic partial order reduction with context-sensitive independence and observers. - Elvira Albert; Maria Garcia de la Banda; Miguel Gómez-Zamalloa; Miguel Isabel; Peter J. Stuckey (J. Syst. Softw., 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)

SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. - Elvira Albert; Maria Garcia de la Banda; Alejandro Hernández-Cerezo; Alexey Ignatiev; Albert Rubio; Peter J. Stuckey (Proc. ACM Program. Lang., 2024)

Artifact for "SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-based, and SAT Techniques". - Elvira Albert; Maria Garcia de la Banda; Alejandro Hernández-Cerezo; Alexey Ignatiev; Albert Rubio; Peter J. Stuckey (Zenodo, 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)

Secure Optimizations on Ethereum Bytecode Jump-Free Sequences. - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (IEEE Trans. Dependable Secur. Comput., 2025)

Certified Cost Bounds for Abstract Programs. - Elvira Albert; Reiner Hähnle; Alicia Merayo; Dominic Steinhöfel (ACM Trans. Softw. Eng. Methodol., 2025)