Elvira Albert
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
85
Venues
30
Active years
1998–2026
Best venue rank
A*
Where they publish
- CLOPSTR14 papers
- BSAS7 papers
- A*CAV6 papers
- BLPAR6 papers
- BFM5 papers
- ATACAS5 papers
- BATVA4 papers
- BICLP4 papers
- CPEPM4 papers
- AISSTA3 papers
- CFORTE3 papers
- BFASE2 papers
- BIFM2 papers
- CPPDP2 papers
- CPADL2 papers
- BAPLAS2 papers
- BSEFM1 paper
- ACADE1 paper
- AICST1 paper
- CVECoS1 paper
- BCC1 paper
- CISoLA1 paper
- CFMICS1 paper
- BVMCAI1 paper
- MulticonferenceSAC1 paper
- CSCAM1 paper
- AESOP1 paper
- BEuroPar1 paper
- BSMC1 paper
- NationalFLOPS1 paper
Papers
85 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | FM | Towards Formally Verified Smart Contracts Compilation. | Elvira Albert, Samir Genaim, Enrique Martin-Martin |
| 2025 | LOPSTR | Verifying Smart Contracts in Yul via Transformation to CHC by Interpreter Specialization. | Elvira Albert, Emanuele De Angelis, Fabio Fioravanti, Alejandro Hernndez-Cerezo, Giulia Matricardi |
| 2025 | SEFM | Securely Optimized (Ethereum) Smart Contracts Using Formal Methods. | Elvira Albert, Samir Genaim, Pablo Gordillo, Alejandro Hernndez-Cerezo, Enrique Martin-Martin, Albert Rubio |
| 2024 | ISSTA | Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2023 | CAV | Formally Verified EVM Block-Optimizations. | Elvira Albert, Samir Genaim, Daniel Kirchner, Enrique Martin-Martin |
| 2023 | TACAS | Inferring Needless Write Memory Accesses on Ethereum Bytecode. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2022 | CADE | Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. | Elvira Albert, Pablo Gordillo, Alejandro Hernndez-Cerezo, Clara Rodrguez-Nez, Albert Rubio |
| 2022 | CAV | Distilling Constraints in Zero-Knowledge Protocols. | Elvira Albert, Marta Bells-Muoz, Miguel Isabel, Clara Rodrguez-Nez, Albert Rubio |
| 2022 | TACAS | A Max-SMT Superoptimizer for EVM handling Memory and Storage. | Elvira Albert, Pablo Gordillo, Alejandro Hernndez-Cerezo, Albert Rubio |
| 2021 | CAV | Lower-Bound Synthesis Using Loop Specialization and Max-SMT. | Elvira Albert, Samir Genaim, Enrique Martin-Martin, Alicia Merayo, Albert Rubio |
| 2021 | FASE | Certified Abstract Cost Analysis. | Elvira Albert, Reiner Hhnle, Alicia Merayo, Dominic Steinhfel |
| 2020 | CAV | Synthesis of Super-Optimized Smart Contracts Using Max-SMT. | Elvira Albert, Pablo Gordillo, Albert Rubio, Maria Anna Schett |
| 2020 | ICST | Smart, and also Reliable and Gas-Efficient, Contracts. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2020 | TACAS | GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2019 | ISSTA | Optimal context-sensitive dynamic partial order reduction with observers. | Elvira Albert, Maria Garcia de la Banda, Miguel Gmez-Zamalloa, Miguel Isabel, Peter J. Stuckey |
| 2019 | ISSTA | SAFEVM: a safety verifier for Ethereum smart contracts. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2019 | VECoS | Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. | Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey |
| 2018 | ATVA | EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. | Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey |
| 2018 | CAV | Constrained Dynamic Partial Order Reduction. | Elvira Albert, Miguel Gmez-Zamalloa, Miguel Isabel, Albert Rubio |
| 2018 | FM | SDN-Actors: Modeling and Verification of SDN Programs. | Elvira Albert, Miguel Gmez-Zamalloa, Albert Rubio, Matteo Sammartino, Alexandra Silva |
| 2017 | ATVA | May-Happen-in-Parallel Analysis with Returned Futures. | Elvira Albert, Samir Genaim, Pablo Gordillo |
| 2017 | CAV | Context-Sensitive Dynamic Partial Order Reduction. | Elvira Albert, Puri Arenas, Maria Garcia de la Banda, Miguel Gmez-Zamalloa, Peter J. Stuckey |
| 2017 | LOPSTR | Generation of Initial Contexts for Effective Deadlock Detection. | Elvira Albert, Miguel Gmez-Zamalloa, Miguel Isabel |
| 2016 | CC | SYCO: a systematic testing tool for concurrent objects. | Elvira Albert, Miguel Gmez-Zamalloa, Miguel Isabel |
| 2016 | IFM | Combining Static Analysis and Testing for Deadlock Detection. | Elvira Albert, Miguel Gmez-Zamalloa, Miguel Isabel |
| 2016 | LOPSTR | A Formal, Resource Consumption-Preserving Translation of Actors to Haskell. | Elvira Albert, Nikolaos Bezirgiannis, Frank S. de Boer, Enrique Martin-Martin |
| 2016 | PPDP | Testing of concurrent and imperative software using CLP. | Elvira Albert, Puri Arenas, Miguel Gmez-Zamalloa |
| 2015 | ATVA | Test Case Generation of Actor Systems. | Elvira Albert, Puri Arenas, Miguel Gmez-Zamalloa |
| 2015 | FM | Resource Analysis: From Sequential to Concurrent and Distributed Programs. | Elvira Albert, Puri Arenas, Jess Correas, Samir Genaim, Miguel Gmez-Zamalloa, Enrique Martin-Martin, Germn Puebla, Guillermo Romn-Dez |
| 2015 | SAS | Parallel Cost Analysis of Distributed Systems. | Elvira Albert, Jess Correas, Einar Broch Johnsen, Guillermo Romn-Dez |
| 2015 | SAS | May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. | Elvira Albert, Samir Genaim, Pablo Gordillo |
| 2015 | TACAS | Non-cumulative Resource Analysis. | Elvira Albert, Jess Correas Fernndez, Guillermo Romn-Dez |
| 2014 | FORTE | Actor- and Task-Selection Strategies for Pruning Redundant State-Exploration in Testing. | Elvira Albert, Puri Arenas, Miguel Gmez-Zamalloa |
| 2014 | ISoLA | Static Inference of Transmission Data Sizes in Distributed Systems. | Elvira Albert, Jess Correas Fernndez, Enrique Martin-Martin, Guillermo Romn-Dez |
| 2014 | SAS | Peak Cost Analysis of Distributed Systems. | Elvira Albert, Jess Correas Fernndez, Guillermo Romn-Dez |
| 2014 | TACAS | SACO: Static Analyzer for Concurrent Objects. | Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gmez-Zamalloa, Enrique Martin-Martin, German Puebla, Guillermo Romn-Dez |
| 2013 | ATVA | Termination and Cost Analysis of Loops with Concurrent Interleavings. | Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin |
| 2013 | FORTE | May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects. | Antonio Flores-Montoya, Elvira Albert, Samir Genaim |
| 2013 | IFM | Quantified Abstractions of Distributed Systems. | Elvira Albert, Jess Correas, Germn Puebla, Guillermo Romn-Dez |
| 2013 | LOPSTR | A Transformational Approach to Resource Analysis with Typed-Norms. | Elvira Albert, Samir Genaim, Ral Gutirrez |
| 2013 | LPAR | May-Happen-in-Parallel Analysis for Priority-Based Scheduling. | Elvira Albert, Samir Genaim, Enrique Martin-Martin |
| 2012 | FASE | Verified Resource Guarantees for Heap Manipulating Programs. | Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hhnle, Guillermo Romn-Dez |
| 2012 | FMICS | Automated Extraction of Abstract Behavioural Models from JMS Applications. | Elvira Albert, Bjarte M. stvold, Jos Miguel Rojas |
| 2012 | FORTE | Analysis of May-Happen-in-Parallel in Concurrent Objects. | Elvira Albert, Antonio Flores-Montoya, Samir Genaim |
| 2012 | ICLP | Towards Testing Concurrent Objects in CLP. | Elvira Albert, Puri Arenas, Miguel Gmez-Zamalloa |
| 2012 | LPAR | Automatic Inference of Resource Consumption Bounds. | Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gmez-Zamalloa, Germn Puebla |
| 2012 | PADL | Symbolic Execution of Concurrent Objects in CLP. | Elvira Albert, Puri Arenas, Miguel Gmez-Zamalloa |
| 2012 | PEPM | COSTABS: a cost and termination analyzer for ABS. | Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gmez-Zamalloa, Germn Puebla |
| 2012 | PEPM | Incremental resource usage analysis. | Elvira Albert, Jess Correas, Germn Puebla, Guillermo Romn-Dez |
| 2011 | APLAS | Cost Analysis of Concurrent OO Programs. | Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gmez-Zamalloa, German Puebla |
| 2011 | FM | Simulating Concurrent Behaviors with Worst-Case Cost Bounds. | Elvira Albert, Samir Genaim, Miguel Gmez-Zamalloa, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa |
| 2011 | LOPSTR | Resource-Driven CLP-Based Test Case Generation. | Elvira Albert, Miguel Gmez-Zamalloa, Jos Miguel Rojas |
| 2011 | PEPM | Verified resource guarantees using COSTA and KeY. | Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hhnle, Germn Puebla, Guillermo Romn-Dez |
| 2011 | VMCAI | More Precise Yet Widely Applicable Cost Analysis. | Elvira Albert, Samir Genaim, Abu Naser Masud |
| 2010 | LOPSTR | Compositional CLP-Based Test Data Generation for Imperative Languages. | Elvira Albert, Miguel Gmez-Zamalloa, Jos Miguel Rojas, Germn Puebla |
| 2010 | PEPM | PET: a partial evaluation-based test case generation tool for Java bytecode. | Elvira Albert, Miguel Gmez-Zamalloa, Germn Puebla |
| 2010 | SAS | From Object Fields to Local Variables: A Practical Approach to Field-Sensitive Analysis. | Elvira Albert, Puri Arenas, Samir Genaim, German Puebla, Diana V. Ramrez-Deantes |
| 2009 | APLAS | Asymptotic Resource Usage Bounds. | Elvira Albert, Diego Esteban Alonso-Blas, Puri Arenas, Samir Genaim, German Puebla |
| 2009 | FM | Field-Sensitive Value Analysis by Field-Insensitive Analysis. | Elvira Albert, Puri Arenas, Samir Genaim, Germn Puebla |
| 2008 | LOPSTR | Test Data Generation of Bytecode by CLP Partial Evaluation. | Elvira Albert, Miguel Gmez-Zamalloa, Germn Puebla |
| 2008 | SAC | Removing useless variables in cost analysis of Java bytecode. | Elvira Albert, Puri Arenas, Samir Genaim, Germn Puebla, Damiano Zanardini |
| 2008 | SAS | Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. | Elvira Albert, Puri Arenas, Samir Genaim, Germn Puebla |
| 2008 | SCAM | Modular Decompilation of Low-Level Code by Partial Evaluation. | Miguel Gmez-Zamalloa, Elvira Albert, Germn Puebla |
| 2007 | ESOP | Cost Analysis of Java Bytecode. | Elvira Albert, Puri Arenas, Samir Genaim, Germn Puebla, Damiano Zanardini |
| 2007 | LOPSTR | Type-Based Homeomorphic Embedding and Its Applications to Online Partial Evaluation. | Elvira Albert, John P. Gallagher, Miguel Gmez-Zamalloa, Germn Puebla |
| 2007 | PADL | Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. | Elvira Albert, Miguel Gmez-Zamalloa, Laurent Hubert, Germn Puebla |
| 2006 | ICLP | Reduced Certificates for Abstraction-Carrying Code. | Elvira Albert, Puri Arenas-Snchez, Germn Puebla, Manuel V. Hermenegildo |
| 2006 | LPAR | An Incremental Approach to Abstraction-Carrying Code. | Elvira Albert, Puri Arenas, Germn Puebla |
| 2006 | SAS | Abstract Interpretation with Specialized Definitions. | Germn Puebla, Elvira Albert, Manuel V. Hermenegildo |
| 2005 | ICLP | A Generic Framework for the Analysis and Specialization of Logic Programs. | Germn Puebla, Elvira Albert, Manuel V. Hermenegildo |
| 2005 | LOPSTR | Non-leftmost Unfolding in Partial Evaluation of Logic Programs with Impure Predicates. | Elvira Albert, Germn Puebla, John P. Gallagher |
| 2005 | LOPSTR | Converting One Type-Based Abstract Domain to Another. | John P. Gallagher, Germn Puebla, Elvira Albert |
| 2005 | PPDP | Abstraction carrying code and resource-awareness. | Manuel V. Hermenegildo, Elvira Albert, Pedro Lpez-Garca, Germn Puebla |
| 2004 | EuroPar | Some Techniques for Automated, Resource-Aware Distributed and Mobile Computing in a Multi-paradigm Programming System. | Manuel V. Hermenegildo, Elvira Albert, Pedro Lpez-Garca, Germn Puebla |
| 2004 | ICLP | Abstract Interpretation-Based Mobile Code Certification. | Elvira Albert, Germn Puebla, Manuel V. Hermenegildo |
| 2004 | LOPSTR | Efficient Local Unfolding with Ancestor Stacks for Full Prolog. | Germn Puebla, Elvira Albert, Manuel V. Hermenegildo |
| 2004 | LPAR | Abstraction-Carrying Code. | Elvira Albert, Germn Puebla, Manuel V. Hermenegildo |
| 2004 | SMC | Experiments in abstract interpretation-based code certification for pervasive systems. | Elvira Albert, Germn Puebla, Manuel V. Hermenegildo |
| 2001 | FLOPS | A Practical Partial Evaluator for a Multi-Paradigm Declarative Language. | Elvira Albert, Michael Hanus, Germn Vidal |
| 2001 | LOPSTR | Symbolic Profiling for Multi-paradigm Declarative Languages. | Elvira Albert, Germn Vidal |
| 2000 | LOPSTR | Measuring the Effectiveness of Partial Evaluation. | Elvira Albert, Sergio Antoy, Germn Vidal |
| 2000 | LOPSTR | Measuring the Effectiveness of Partial Evaluation in Functional Logic Languages. | Elvira Albert, Sergio Antoy, Germn Vidal |
| 2000 | LPAR | Using an Abstract Representation to Specialize Functional Logic Programs. | Elvira Albert, Michael Hanus, Germn Vidal |
| 1999 | LPAR | A Partial Evaluation Framework for Curry Programs. | Elvira Albert, Mara Alpuente, Michael Hanus, Germn Vidal |
| 1998 | SAS | Improving Control in Functional Logic Program Specialization. | Elvira Albert, Mara Alpuente, Moreno Falaschi, Pascual Julin Iranzo, Germn Vidal |