Elvira Albert

ORCID

Publication Activity (10 Years)

Years Active: 1998-2024
Publications (10 Years): 55

Top Venues

CoRR

Sci. Comput. Program.

ATVA

J. Syst. Softw.

Publications

Elvira Albert, Maria Garcia de la Banda, Alejandro Hernández-Cerezo, Alexey Ignatiev, Albert Rubio, Peter J. Stuckey
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Elvira Albert, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, Miguel Isabel, Peter J. Stuckey
Optimal dynamic partial order reduction with context-sensitive independence and observers. J. Syst. Softw. 202 (2023)
Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv
Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. IEEE Trans. Dependable Secur. Comput. 20 (3) (2023)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
Inferring Needless Write Memory Accesses on Ethereum Bytecode. TACAS (1) (2023)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
Inferring Needless Write Memory Accesses on Ethereum Bytecode (Extended Version). CoRR (2023)
Elvira Albert, Samir Genaim, Daniel Kirchner, Enrique Martin-Martin
Formally Verified EVM Block-Optimizations. CAV (3) (2023)
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez, Albert Rubio
Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. IJCAR (2022)
Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez, Albert Rubio
Distilling Constraints in Zero-Knowledge Protocols. CAV (1) (2022)
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio, Maria Anna Schett
Super-optimization of Smart Contracts. ACM Trans. Softw. Eng. Methodol. 31 (4) (2022)
Elvira Albert, Samir Genaim, Alicia Merayo, Guillermo Román-Díez
When COSTA Met KeY: Verified Cost Bounds. The Logic of Software. A Tasting Menu of Formal Methods (2022)
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio
A Max-SMT Superoptimizer for EVM handling Memory and Storage. TACAS (1) (2022)
Elvira Albert, Reiner Hähnle, Alicia Merayo, Dominic Steinhöfel
Certified Abstract Cost Analysis. FASE (2021)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
- Parametric gas bounds for smart contracts. J. Syst. Softw. 176 (2021)
Elvira Albert, Samir Genaim, Enrique Martin-Martin, Alicia Merayo, Albert Rubio
Lower-Bound Synthesis Using Loop Specialization and Max-SMT. CAV (2) (2021)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio, Matteo Sammartino, Alexandra Silva
Actor-based model checking for Software-Defined Networks. J. Log. Algebraic Methods Program. 118 (2021)
Elvira Albert, Samir Genaim, Raúl Gutiérrez, Enrique Martin-Martin
A Transformational Approach to Resource Analysis with Typed-norms Inference. Theory Pract. Log. Program. 20 (3) (2020)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
Smart, and also Reliable and Gas-Efficient, Contracts. ICST (2020)
Elvira Albert, Pablo Gordillo, Albert Rubio, Maria Anna Schett
Synthesis of Super-Optimized Smart Contracts Using Max-SMT. CAV (1) (2020)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph. CoRR (2020)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio, Matteo Sammartino, Alexandra Silva
Actor-Based Model Checking for SDN Networks. CoRR (2020)
Elvira Albert, Nikolaos Bezirgiannis, Frank S. de Boer, Enrique Martin-Martin
A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell. Fundam. Informaticae 177 (3-4) (2020)
Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv
Taming callbacks for smart contract modularity. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. TACAS (2) (2020)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
SAFEVM: a safety verifier for Ethereum smart contracts. ISSTA (2019)
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. VECoS (2019)
Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, Albert Rubio
Resource Analysis driven by (Conditional) Termination Proofs. Theory Pract. Log. Program. 19 (5-6) (2019)
Elvira Albert, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, Miguel Isabel, Peter J. Stuckey
Optimal context-sensitive dynamic partial order reduction with observers. ISSTA (2019)
Elvira Albert, Samir Genaim, Raúl Gutiérrez, Enrique Martin-Martin
A Transformational Approach to Resource Analysis with Typed-norms Inference. CoRR (2019)
Elvira Albert, Jesús Correas, Guillermo Román-Díez
Peak resource analysis of concurrent distributed systems. J. Syst. Softw. 149 (2019)
Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, Albert Rubio
Resource Analysis driven by (Conditional) Termination Proofs. CoRR (2019)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. CoRR (2019)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
SAFEVM: A Safety Verifier for Ethereum Smart Contracts. CoRR (2019)
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
GASTAP: A Gas Analyzer for Smart Contracts. CoRR (2018)
Elvira Albert, Jesús Correas, Einar Broch Johnsen, Violet Ka I Pun, Guillermo Román-Díez
Parallel Cost Analysis. ACM Trans. Comput. Log. 19 (4) (2018)
Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. ATVA (2018)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio
Constrained Dynamic Partial Order Reduction. CAV (2) (2018)
Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. CoRR (2018)
Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa
Systematic testing of actor systems. Softw. Test. Verification Reliab. 28 (3) (2018)
Elvira Albert, Miguel Gómez-Zamalloa, Albert Rubio, Matteo Sammartino, Alexandra Silva
SDN-Actors: Modeling and Verification of SDN Programs. FM (2018)
Elvira Albert, Puri Arenas, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, Peter J. Stuckey
Context-Sensitive Dynamic Partial Order Reduction. CAV (1) (2017)
Elvira Albert
Preface for selected and extended papers from Principles and Practice of Declarative Programming (PPDP'15). Sci. Comput. Program. 147 (2017)
Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin
Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings. J. Autom. Reason. 59 (1) (2017)
Elvira Albert, Samir Genaim, Pablo Gordillo
May-Happen-in-Parallel Analysis with Returned Futures. ATVA (2017)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel
Generation of Initial Contexts for Effective Deadlock Detection. LOPSTR (2017)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel
On the Generation of Initial Contexts for Effective Deadlock Detection. CoRR (2017)
Elvira Albert, Pablo C. Cañizares, Esther Guerra, Juan de Lara, Esperanza Marcos, Manuel Núñez, Guillermo Román-Díez, Juan Manuel Vara, Damiano Zanardini
SICOMORo-CM: Development of Trustworthy Systems via Models and Advanced Tools. STAF Workshops (2017)
Elvira Albert, Jesús Correas, Guillermo Román-Díez
Resource Analysis of Distributed Systems. Theory and Practice of Formal Methods (2016)
Damiano Zanardini, Elvira Albert, Karina Villela
Resource-usage-aware configuration in software product lines. J. Log. Algebraic Methods Program. 85 (1) (2016)
Elvira Albert, Nikolaos Bezirgiannis, Frank S. de Boer, Enrique Martin-Martin
A Formal, Resource Consumption-Preserving Translation of Actors to Haskell. LOPSTR (2016)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel
Combining Static Analysis and Testing for Deadlock Detection. IFM (2016)
Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, Guillermo Román-Díez
A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY. Softw. Syst. Model. 15 (4) (2016)
Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin
May-Happen-in-Parallel Analysis for Actor-Based Concurrency. ACM Trans. Comput. Log. 17 (2) (2016)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel
SYCO: a systematic testing tool for concurrent objects. CC (2016)
Elvira Albert, Nikolaos Bezirgiannis, Frank S. de Boer, Enrique Martin-Martin
A Formal, Resource Consumption-Preserving Translation of Actors to Haskell. CoRR (2016)
Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa
Testing of concurrent and imperative software using CLP. PPDP (2016)
Elvira Albert, Jesús Correas Fernández, Germán Puebla, Guillermo Román-Díez
A multi-domain incremental analysis engine and its application to incremental resource analysis. Theor. Comput. Sci. 585 (2015)
Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla
A practical comparator of cost functions and its applications. Sci. Comput. Program. 111 (2015)
Elvira Albert, Antonio Flores-Montoya, Samir Genaim
May-Happen-in-Parallel Analysis with Condition Synchronization. FOPARA (2015)
Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa
Test Case Generation of Actor Systems. ATVA (2015)
Elvira Albert, Puri Arenas, Jesús Correas Fernández, Samir Genaim, Miguel Gómez-Zamalloa, Germán Puebla, Guillermo Román-Díez
Object-sensitive cost analysis for concurrent objects. Softw. Test. Verification Reliab. 25 (3) (2015)
Elvira Albert, Samir Genaim, Pablo Gordillo
May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. SAS (2015)
Elvira Albert, Jesús Correas Fernández, Germán Puebla, Guillermo Román-Díez
Quantified abstract configurations of distributed systems. Formal Aspects Comput. 27 (4) (2015)
Elvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, Germán Puebla, Guillermo Román-Díez
Resource Analysis: From Sequential to Concurrent and Distributed Programs. FM (2015)
Elvira Albert, Jesús Correas, Einar Broch Johnsen, Guillermo Román-Díez
Parallel Cost Analysis of Distributed Systems. SAS (2015)
Elvira Albert, Jesús Correas Fernández, Guillermo Román-Díez
Non-cumulative Resource Analysis. TACAS (2015)
Elvira Albert, Jesús Correas Fernández, Guillermo Román-Díez
Peak Cost Analysis of Distributed Systems. SAS (2014)
Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa
Actor- and Task-Selection Strategies for Pruning Redundant State-Exploration in Testing. FORTE (2014)
Elvira Albert, Frank S. de Boer, Reiner Hähnle, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, Peter Y. H. Wong
Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS. Serv. Oriented Comput. Appl. 8 (4) (2014)
Elvira Albert, Jesús Correas Fernández, Enrique Martin-Martin, Guillermo Román-Díez
Static Inference of Transmission Data Sizes in Distributed Systems. ISoLA (2) (2014)
Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, German Puebla, Guillermo Román-Díez
SACO: Static Analyzer for Concurrent Objects. TACAS (2014)
Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, Guillermo Román-Díez
Conditional termination of loops over heap-allocated data. Sci. Comput. Program. 92 (2014)
Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa, José Miguel Rojas
Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency. SFM (2014)
Elvira Albert, Shin-Cheng Mu
Selected and extended papers from Partial Evaluation and Program Manipulation 2013. Sci. Comput. Program. 95 (2014)
Elvira Albert, Samir Genaim, Enrique Martin-Martin
May-Happen-in-Parallel Analysis for Priority-Based Scheduling. LPAR (2013)
Elvira Albert, Jesús Correas, Germán Puebla, Guillermo Román-Díez
Quantified Abstractions of Distributed Systems. IFM (2013)
Elvira Albert, Frank S. de Boer, Reiner Hähnle, Einar Broch Johnsen, Cosimo Laneve
Engineering virtualized services. NordiCloud (2013)
Elvira Albert, Samir Genaim, Miguel Gómez-Zamalloa
Heap space analysis for garbage collected languages. Sci. Comput. Program. 78 (9) (2013)
Elvira Albert, Samir Genaim, Abu Naser Masud
On the Inference of Resource Usage Upper and Lower Bounds. ACM Trans. Comput. Log. 14 (3) (2013)
Antonio Flores-Montoya, Elvira Albert, Samir Genaim
May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects. FMOODS/FORTE (2013)
Elvira Albert, Samir Genaim, Raúl Gutiérrez
A Transformational Approach to Resource Analysis with Typed-Norms. LOPSTR (2013)
Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin
Termination and Cost Analysis of Loops with Concurrent Interleavings. ATVA (2013)
Elvira Albert, Maria J. García de la Banda, Miguel Gómez-Zamalloa, José Miguel Rojas, Peter J. Stuckey
A CLP heap solver for test case generation. Theory Pract. Log. Program. 13 (4-5) (2013)
Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa, Peter Y. H. Wong
aPET: a test case generation tool for concurrent objects. ESEC/SIGSOFT FSE (2013)
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
Automatic Inference of Bounds on Resource Consumption. FMCO (2012)
Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa
Symbolic Execution of Concurrent Objects in CLP. PADL (2012)
Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gómez-Zamalloa, Germán Puebla
COSTABS: a cost and termination analyzer for ABS. PEPM (2012)
Elvira Albert, Puri Arenas, Germán Puebla, Manuel V. Hermenegildo
Certificate size reduction in abstraction-carrying code. Theory Pract. Log. Program. 12 (3) (2012)
Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Guillermo Román-Díez
Verified Resource Guarantees for Heap Manipulating Programs. FASE (2012)
Peter Y. H. Wong, Elvira Albert, Radu Muschevici, José Proença, Jan Schäfer, Rudolf Schlatte
The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. Int. J. Softw. Tools Technol. Transf. 14 (5) (2012)
Elvira Albert, Puri Arenas, Samir Genaim, German Puebla, Damiano Zanardini
Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413 (1) (2012)
Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gómez-Zamalloa, Germán Puebla
Automatic Inference of Resource Consumption Bounds. LPAR (2012)
Elvira Albert, Jesús Correas, Germán Puebla, Guillermo Román-Díez
Incremental resource usage analysis. PEPM (2012)
Elvira Albert, Bjarte M. Østvold, José Miguel Rojas
Automated Extraction of Abstract Behavioural Models from JMS Applications. FMICS (2012)
Elvira Albert, Antonio Flores-Montoya, Samir Genaim
MayPar: a may-happen-in-parallel analyzer for concurrent objects. SIGSOFT FSE (2012)
Elvira Albert, Antonio Flores-Montoya, Samir Genaim
Analysis of May-Happen-in-Parallel in Concurrent Objects. FMOODS/FORTE (2012)
Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa
Towards Testing Concurrent Objects in CLP. ICLP (Technical Communications) (2012)
Germán Puebla, Elvira Albert, Manuel V. Hermenegildo
Efficient local unfolding with ancestor stacks. Theory Pract. Log. Program. 11 (1) (2011)
Elvira Albert, Miguel Gómez-Zamalloa, José Miguel Rojas
Resource-Driven CLP-Based Test Case Generation. LOPSTR (2011)
Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla
Closed-Form Upper Bounds in Static Cost Analysis. J. Autom. Reason. 46 (2) (2011)
Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gómez-Zamalloa, German Puebla
Cost Analysis of Concurrent OO Programs. APLAS (2011)

Elvira Albert.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Elvira Albert