International Journals

[1] Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio, and Maria A. Schett. Super-Optimization of Smart Contracts. ACM Transactions on Software Engineering and Methodology, 31 Issue 4(70):1-29, 2022. [ bibtex | abstract | DOI | http ]

[2] Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Albert Rubio. Don't Run on Fumes - Parametric Gas Bounds for Smart Contracts. Journal of Systems and Software, 176:110923, 2021. [ bibtex | abstract | DOI | PDF ]

[3] Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio, Matteo Sammartino, and Alexandra Silva. Actor-based model checking for Software-Defined Networks. J. Log. Algebraic Methods Program., 118:100617, 2021. [ bibtex | abstract | DOI | PDF | http ]

[4] Elvira Albert, Nikolaos Bezirgiannis, Frank de Boer, and Enrique Martin-Martin. A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell. Fundamenta Informaticae, 177(3-4):203-234, 2020. [ bibtex | abstract | DOI | http ]
[5] Elvira Albert, Samir Genaim, Raúl Gutiérrez, and Enrique Martin-Martin. A Transformational Approach to Resource Analysis with Typed-norms Inference. Theory and Practice of Logic Programming, 20(3):310-357, 2020. [ bibtex | abstract | DOI ]
[6] Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, and Albert Rubio. Resource Analysis driven by (Conditional) Termination Proofs. Theory and Practice of Logic Programming, 19(5-6):722-739, 2019. [ bibtex | abstract | DOI ]
[7] Elvira Albert, Jesús Correas, and Guillermo Román-Díez. Peak Resource Analysis of Concurrent Distributed Systems. Journal of Systems and Software, 149:35 - 62, 2019. [ bibtex | abstract | DOI ]

[8] Elvira Albert, Jesús Correas, Einar Broch Johnsen Ka I Pun, and Guillermo Román-Díez. Parallel Cost Analysis. ACM Transactions on Computational Logic, 19(4):1 - 37, 2018. [ bibtex | abstract | DOI ]

[9] Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Systematic testing of actor systems. Software Testing, Verification and Reliability, 2018. [ bibtex | abstract | DOI | http ]

[10] Elvira Albert, Antonio Flores-Montoya, Samir Genaim, and Enrique Martin-Martin. Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings. Journal of Automated Reasoning, 59(1):47-85, Jun 2017. [ bibtex | abstract | DOI | PDF | http ]

[11] Elvira Albert, Antonio Flores-Montoya, Samir Genaim, and Enrique Martin-Martin. May-Happen-in-Parallel Analysis for Actor-based Concurrency. ACM Transactions on Computational Logic, 17(2):11:1-11:39, March 2016. [ bibtex | abstract | DOI | PDF | http ]

[12] Damiano Zanardini, Elvira Albert, and Karina Villela. Resource-Usage-Aware Configuration in Software Product Lines. Journal of Logical and Algebraic Methods in Programming, 85(1, Part 2):173-199, 2016. Formal Methods for Software Product Line Engineering. [ bibtex | abstract | DOI | PDF | http ]

[13] Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, and Guillermo Román-Díez. A Formal Verification Framework for Static Analysis. Software and Systems Modeling, 15(4):987-1012, 2016. [ bibtex | abstract | DOI | PDF | http ]

[14] Elvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel Gómez-Zamalloa, and Germán Puebla an d Guillermo Román-Díez. Object-Sensitive Cost Analysis for Concurrent Objects. Software Testing, Verification and Reliability, 25(3):218-271, 2015. [ bibtex | abstract | DOI | PDF | http ]

[15] Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. A Practical Comparator of Cost Functions and Its Applications. Science of Computer Programming, 111(3):483-504, 2015. [ bibtex | abstract | DOI | PDF | http ]

[16] Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Díez. Quantified Abstract Configurations of Distributed Systems. Formal Aspects of Computing, 27(4):665-699, 2015. [ bibtex | abstract | DOI | PDF | http ]

[17] Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Díez. A Multi-Domain Incremental Analysis Engine and its Application to Incremental Resource Analysis. Theoretical Computer Science, 585(0):91 - 114, 2015. [ bibtex | abstract | DOI | PDF | http ]

[18] Elvira Albert, Frank S. de Boer, Reiner Hähnle, Einar Broch Johnsen, Rudolf Schlatte, S. Lizeth Tapia Tarifa, and Peter Y. H. Wong. Formal Modeling and Analysis of Resource Management for Cloud Architectures. Journal of Service Oriented Computing and Applications, 8(4):323-339, 2014. [ bibtex | abstract | DOI | PDF | http ]

[19] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Guillermo Román-Díez. Conditional Termination of Loops over Heap-allocated Data. Science of Computer Programming, 92:2 - 24, 2014. [ bibtex | abstract | DOI | PDF | http ]

[20] Elvira Albert, María García de la Banda, Miguel Gómez-Zamalloa, José Miguel Rojas, and Peter J. Stuckey. A CLP Heap Solver for Test Case Generation. Theory and Practice of Logic Programming, 13(4-5):721-735, July 2013. [ bibtex | abstract | DOI | PDF | http ]

[21] Elvira Albert, Samir Genaim, and Miguel Gómez-Zamalloa. Heap Space Analysis for Garbage Collected Languages. Science of Computer Programming, 78(9):1427-1448, 2013. [ bibtex | abstract | PDF | http ]

[22] Elvira Albert, Samir Genaim, and Abu Naser Masud. On the Inference of Resource Usage Upper and Lower Bounds. ACM Transactions on Computational Logic, 14(3):22:1-22:35, 2013. [ bibtex | abstract | DOI | PDF | http ]

[23] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. Cost Analysis of Object-Oriented Bytecode Programs. Theoretical Computer Science (Special Issue on Quantitative Aspects of Programming Languages), 413(1):142-159, 2012. [ bibtex | abstract | DOI | PDF | http ]

[24] Peter Y. H. Wong, Elvira Albert, Radu Muschevici, José Proença, Jan Schäfer, and Rudolf Schlatte. The ABS Tool Suite: Modelling, Executing and Analysing Distributed Adaptable Object-Oriented Systems. International Journal on Software Tools for Technology Transfer, 14(5):567-588, 2012. [ bibtex | abstract | DOI ]

[25] Elvira Albert, Puri Arenas, Germán Puebla, and Manuel V. Hermenegildo. Certificate size reduction in abstraction-carrying code. TPLP, 12(3):283-318, 2012. [ bibtex | abstract | DOI ]

[26] Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning, 46(2):161-203, 2011. [ bibtex | abstract | DOI | PDF ]

[27] Elvira Albert, Puri Arenas, Samir Genaim, and Damiano Zanardini. Task-Level Analysis for a Language with Async-Finish Parallelism. ACM SIGPLAN Notices, 46(5):21-30, 2011. [ bibtex | abstract | DOI | PDF ]

[28] Germán Puebla, Elvira Albert, and Manuel V. Hermenegildo. Efficient local unfolding with ancestor stacks. Theory and Practice of Logic Programming, 11(1):1-32, 2011. [ bibtex | abstract | DOI ]

[29] Miguel Gómez-Zamalloa, Elvira Albert, and Germán Puebla. Test Case Generation for Object-Oriented Imperative Languages in CLP. Theory and Practice of Logic Programming, 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue, 10(4-6):659-674, July 2010. [ bibtex | abstract | DOI | PDF ]

[30] Elvira Albert, Samir Genaim, and Miguel Gómez-Zamalloa. Parametric Inference of Memory Requirements for Garbage Collected Languages. ACM SIGPLAN Notices, 45(8):121-130, 2010. [ bibtex | abstract | PDF ]

[31] Miguel Gómez-Zamalloa, Elvira Albert, and Germán Puebla. Decompilation of Java Bytecode to Prolog by Partial Evaluation. Information and Software Technology, 51(10):1409-1427, October 2009. [ bibtex | abstract | DOI | PDF ]
[32] Elvira Albert, John P. Gallagher, Miguel Gómez-Zamalloa, and Germán Puebla. Type-based Homeomorphic Embedding for Online Termination. Information Processing Letters, 109(15):879-886, July 2009. [ bibtex | abstract | DOI | PDF ]
[33] Elvira Albert, Germán Puebla, and Manuel V. Hermenegildo. Abstraction-Carrying Code: a Model for Mobile Code Safety. New Generation Computing, 26(2):171-204, 2008. [ bibtex | abstract | DOI ]

[34] Elvira Albert, Michael Hanus, Frank Huch, Javier Oliver, and Germán Vidal. Operational semantics for declarative multi-paradigm languages. Journal of Symbolic Computation, 40(1):795-829, 2005. [ bibtex | abstract | DOI ]

[35] Elvira Albert, Michael Hanus, and Germán Vidal. A residualizing semantics for the partial evaluation of functional logic programs. Information Processing Letters, 85(1):19-25, 2003. [ bibtex | abstract | DOI ]

[36] Elvira Albert, Michael Hanus, and Germán Vidal. A Practical Partial Evaluation Scheme for Multi-Paradigm Declarative Languages. Journal of Functional and Logic Programming, 2002, 2002. [ bibtex | abstract | DOI | DOI ]

[37] Elvira Albert. Partial evaluation of multi-paradigm declarative languages. AI Communications, 14(4):235-237, 2001. [ bibtex | abstract | DOI ]

[38] Elvira Albert and Germán Vidal. The Narrowing-driven Approach to Functional Logic Program Specialization. New Generation Computing, 20(1):3-26, 2001. [ bibtex | abstract | DOI ]

International Conferences

[1] Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Albert Rubio. Inferring Needless Write Memory Accesses on Ethereum Smart Contracts. In 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023. Proceedings, Lecture Notes in Computer Science. Springer, 2022. To appear. [ bibtex | abstract ]

[2] Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez, and Albert Rubio. Distilling Constraints in Zero-Knowledge Protocols. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 430-443. Springer, 2022. [ bibtex | abstract | DOI | http ]
[3] Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez, and Albert Rubio. Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 3-7. Springer, 2022. [ bibtex | abstract | DOI | PDF ]
[4] Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, and Albert Rubio. A Max-SMT Superoptimizer for EVM handling Memory and Storage. In Dana Fisman and Grigore Rosu, editors, 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022. Proceedings, volume 13243 of Lecture Notes in Computer Science, pages 201-219. Springer, 2022. [ bibtex | abstract | DOI | PDF ]

[5] Elvira Albert, Samir Genaim, Enrique Martín-Martín, Alicia Merayo, and Albert Rubio. Lower-Bound Synthesis Using Loop Specialization and Max-SMT. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pages 863-886. Springer, 2021. [ bibtex | abstract | DOI | http ]

[6] Elvira Albert, Reiner Hähnle, Alicia Merayo, and Dominic Steinhöfel. Certified Abstract Cost Analysis. In Esther Guerra and Mariëlle Stoelinga, editors, Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12649 of Lecture Notes in Computer Science, pages 24-45. Springer, 2021. [ bibtex | abstract | DOI | http ]

[7] Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Nú nez, Albert Rubio, and Mooly Sagiv. Taming Callbacks for Smart Contract Modularity. In ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2020. Proceedings, volume 4, 2020. To appear. [ bibtex | abstract | DOI ]

[8] Elvira Albert, Pablo Gordillo, Albert Rubio, and Maria A. Schett. Synthesis of Super-Optimized Smart Contracts using Max-SMT. In 32nd International Conference on Computer Aided Verification, CAV 2020. Proceedings, volume 12224 of Lecture Notes in Computer Science, pages 177-200, 2020. [ bibtex | abstract | DOI | PDF ]

[9] Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Albert Rubio. GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. In Armin Biere and David Parker, editors, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020. Proceedings, volume 12079 of Lecture Notes in Computer Science, pages 118-125. Springer, 2020. [ bibtex | abstract | DOI | PDF ]

[10] Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Albert Rubio. Smart, and also reliable and gas-efficient, contracts. In 13th IEEE International Conference on Software Testing, Validation and Verification, ICST 2020. Proceedings, IEEE, 2020. [ bibtex | abstract | DOI | PDF ]
[11] Elvira Albert, Pablo Gordillo, Albert Rubio, and Ilya Sergey. Running on Fumes: Preventing Out-Of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis. In Pierre Ganty and Mohamed Kaâniche, editors, 13th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2019. Proceedings, volume 11847 of Lecture Notes in Computer Science, pages 63-78. Springer, 2019. [ bibtex | abstract | DOI | PDF ]

[12] Elvira Albert, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, Miguel Isabel, and Peter J. Stuckey. Optimal Context-Sensitive Dynamic Partial Order Reduction with Observers. In Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis 2019 (ISSTA'19), ACM, pages 352-362, 2019. [ bibtex | abstract | DOI | PDF ]
[13] Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Albert Rubio. SAFEVM: A Safety Verifier for Ethereum Smart Contracts. In Dongmei Zhang and Anders Møller, editors, ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019. Proceedings, ACM, pages 386-389, 2019. [ bibtex | abstract | DOI | PDF ]

[14] Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, and Ilya Sergey. EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. In Shuvendu Lahiri and Chao Wang, editors, 16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018. Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 513-520. Springer, 2018. [ bibtex | abstract | DOI | PDF ]

[15] Elvira Albert, Miguel Gómez-Zamalloa, Albert Rubio, Matteo Sammartino, and Alexandra Silva. SDN-Actors: Modeling and Verification of SDN Programs. In Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings, pages 550-567, 2018. [ bibtex | abstract | DOI | http ]
[16] Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, and Albert Rubio. Constrained Dynamic Partial Order Reduction. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 392-410. Springer, 2018. [ bibtex | abstract | DOI | PDF | http ]
[17] Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. Generation of Initial Contexts for Effective Deadlock Detection. In Logic-Based Program Synthesis and Transformation: 27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised Selected Papers, volume 10855 of Lecture Notes in Computer Science, pages 3-19. Springer International Publishing, 2018. [ bibtex | abstract | DOI | PDF ]
[18] Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. On the Generation of Initial Contexts for Effective Deadlock Detection. In LOPSTR 2017, October 2017. Extended abstract. [ bibtex | abstract | PDF ]
[19] Elvira Albert, Puri Arenas, María García de la Banda, Miguel Gómez-Zamalloa, and Peter J. Stuckey. Context Sensitive Dynamic Partial Order Reduction. In Victor Kuncak and Rupak Majumdar, editors, 29th International Conference on Computer Aided Verification (CAV 2017), volume 10426 of Lecture Notes in Computer Science, pages 526-543. Springer, 2017. [ bibtex | abstract | DOI | http ]
[20] Elvira Albert, Samir Genaim, and Pablo Gordillo. May-Happen-in-Parallel Analysis with Returned Futures. In Deepak D'Souza and K.Narayan Kumar, editors, 15th International Symposium on Automated Technology for Verification and Analysis, ATVA 2017. Proceedings, volume 10482 of Lecture Notes in Computer Science, pages 42-58. Springer, 2017. [ bibtex | abstract | DOI | PDF ]

[21] Elvira Albert, Nikolaos Bezirgiannis, Frank de Boer, and Enrique Martin-Martin. A Formal, Resource Consumption-Preserving Translation of Actors to Haskell. In Manuel V Hermenegildo and Pedro Lopez-Garcia, editors, Logic-Based Program Synthesis and Transformation: 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers, volume 10184 of Lecture Notes in Computer Science, pages 21-37. Springer International Publishing, 2017. [ bibtex | abstract | DOI | http ]
[22] Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Testing of Concurrent and Imperative Software Using CLP. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, pages 1-8. ACM, 2016. [ bibtex | abstract | DOI | PDF | http ]
[23] Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. Combining Static Analysis and Testing for Deadlock Detection. In Erika Ábrahám and Marieke Huisman, editors, Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings, volume 9681 of Lecture Notes in Computer Science, pages 409-424. Springer, 2016. [ bibtex | abstract | DOI | PDF | http ]

[24] Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. SYCO: A Systematic Testing Tool for Concurrent Objects. In Ayal Zaks and Manuel V. Hermenegildo, editors, Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12-18, 2016, pages 269-270. ACM, 2016. [ bibtex | abstract | DOI | PDF | http ]

[25] Elvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, Germán Puebla, and Guillermo Román-Díez. Resource Analysis: From Sequential to Concurrent and Distributed Programs. In Nikolaj Bjørner and Frank D. de Boer, editors, FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 3-17. Springer, 2015. [ bibtex | abstract | DOI | PDF | http ]
[26] Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Test Case Generation of Actor Systems. In 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015. Proceedings, volume 9364 of Lecture Notes in Computer Science, pages 259-275. Springer, 2015. [ bibtex | abstract | DOI | PDF | http ]

[27] Elvira Albert, Samir Genaim, and Pablo Gordillo. May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. In Sandrine Blazy and Thomas P. Jensen, editors, Static Analysis - 22nd International Symposium, SAS 2015. Proceedings, volume 9291 of Lecture Notes in Computer Science, pages 72-89. Springer, 2015. [ bibtex | abstract | DOI | PDF | http ]

[28] Elvira Albert, Jesús Correas, Einar Broch Johnsen, and Guillermo Román-Díez. Parallel Cost Analysis of Distributed Systems. In Static Analysis - 22nd International Symposium, SAS 2015. Proceedings, volume 9291 of Lecture Notes in Computer Science, pages 275-292. Springer, 2015. [ bibtex | abstract | DOI | PDF | http ]

[29] Elvira Albert, Jesús Correas, and Guillermo Román-Díez. Non-Cumulative Resource Analysis. In Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), volume 9035 of Lecture Notes in Computer Science, pages 85-100. Springer, 2015. [ bibtex | abstract | DOI | PDF | http ]

[30] Elvira Albert, Jesús Correas, Enrique Martín-Martín, and Guillermo Román-Díez. Static Inference of Transmission Data Sizes in Distributed Systems. In 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'14), volume 8803 of Lecture Notes in Computer Science, pages 104-119. Springer, 2014. [ bibtex | abstract | DOI | PDF | http ]

[31] Elvira Albert, Jesús Correas, and Guillermo Román-Díez. Peak Cost Analysis of Distributed Systems. In Markus Müller-Olm and Helmut Seidl, editors, Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, volume 8723 of Lecture Notes in Computer Science, pages 18-33. Springer, 2014. [ bibtex | abstract | DOI | PDF | http ]

[32] Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Actor- and Task-Selection Strategies for Pruning Redundant State-Exploration in Testing. In Erika Ábrahám and Catuscia Palamidessi, editors, 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE 2014), volume 8461 of Lecture Notes in Computer Science, pages 49-65. Springer, 2014. [ bibtex | abstract | DOI | PDF | http ]

[33] Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, Germán Puebla, and Guillermo Román-Díez. SACO: Static Analyzer for Concurrent Objects. In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, volume 8413 of Lecture Notes in Computer Science, pages 562-567. Springer, 2014. [ bibtex | abstract | DOI | PDF | http ]

[34] Elvira Albert, Samir Genaim, and Raúl Gutiérrez. A Transformational Approach to Resource Analysis with Typed-Norms. In Proc. of the 23rd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'13), volume 8901 of Lecture Notes in Computer Science, pages 38-53. Springer, 2014. [ bibtex | abstract | PDF | http ]

[35] Elvira Albert, Samir Genaim, and Enrique Martin-Martin. May-Happen-in-Parallel Analysis for Priority-based Scheduling. In Ken McMillan, Aart Middeldorp, and Andrei Voronkov, editors, 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19), volume 8312 of Lecture Notes in Computer Science, pages 18-34. Springer, December 2013. [ bibtex | abstract | DOI | PDF | http ]

[36] Antonio Flores-Montoya, Elvira Albert, and Samir Genaim. May-Happen-in-Parallel based Deadlock Analysis for Concurrent Objects. In Dirk Beyer and Michele Boreale, editors, Formal Techniques for Distributed Systems (FMOODS/FORTE 2013), volume 7892 of Lecture Notes in Computer Science, pages 273-288. Springer, June 2013. [ bibtex | abstract | http ]

[37] Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Díez. Quantified Abstractions of Distributed Systems. In 10th International Conference on integrated Formal Methods (iFM'13), volume 7940 of Lecture Notes in Computer Science, pages 285-300. Springer, June 2013. [ bibtex | abstract | DOI | PDF | http ]

[38] Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa, and Peter Y.H. Wong. aPET: A Test Case Generation Tool for Concurrent Objects. In Bertrand Meyer, Luciano Baresi, and Mira Mezini, editors, Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE'13, Saint Petersburg, Russian Federation, August 18-26, 2013, pages 595-598. ACM, 2013. [ bibtex | abstract | DOI | PDF | http ]

[39] Elvira Albert, Antonio Flores-Montoya, Samir Genaim, and Enrique Martin-Martin. Termination and Cost Analysis of Loops with Concurrent Interleavings. In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pages 349-364. Springer, 2013. [ bibtex | abstract | DOI | PDF | http ]

[40] Elvira Albert, Antonio Flores-Montoya, and Samir Genaim. MayPar: a may-happen-in-parallel analyzer for concurrent objects. In Will Tracz, Martin P. Robillard, and Tevfik Bultan, editors, 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), SIGSOFT/FSE'12, Cary, NC, USA - November 11 - 16, 2012, pages 1-4. ACM, November 2012. [ bibtex | abstract | DOI ]

[41] Elvira Albert, Miguel Gómez-Zamalloa, and José Miguel Rojas. Resource-driven CLP-based Test Case Generation. In LOPSTR 2011 Revised Selected Papers, volume 7225 of Lecture Notes in Computer Science, pages 25-41. Springer, July 2012. [ bibtex | abstract | PDF | http ]

[42] Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, and Guillermo Román-Díez. Verified Resource Guarantees for Heap Manipulating Programs. In Proceedings of the 15th International Conference on Fundamental Approaches to Software Engineering, FASE 2012, Tallinn, Estonia, March, 2012, volume 7212 of Lecture Notes in Computer Science, pages 130-145. Springer, March 2012. [ bibtex | abstract | DOI | PDF | http ]

[43] Elvira Albert, Bjarte M. Østvold, and José Miguel Rojas. Automated Extraction of Abstract Behavioural Models from JMS Applications. In Formal Methods for Industrial Critical Systems (FMICS'12), volume 7437 of Lecture Notes in Computer Science, pages 16-31. Springer, 2012. [ bibtex | abstract | PDF ]

[44] Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Towards Testing Concurrent Objects in CLP. In Agostino Dovier and Vítor Santos Costa, editors, 28th International Conference on Logic Programming (ICLP'12), volume 17 of LIPIcs, pages 98-108. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. [ bibtex | abstract | DOI | PDF ]

[45] Elvira Albert, Antonio Flores-Montoya, and Samir Genaim. Analysis of May-Happen-in-Parallel in Concurrent Objects. In Holger Giese and Grigore Rosu, editors, Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings, volume 7273 of Lecture Notes in Computer Science, pages 35-51. Springer, 2012. [ bibtex | abstract | DOI | http ]

[46] Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Díez. Incremental Resource Usage Analysis. In Proceedings of the 2012 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23-24, 2012, pages 25-34. ACM Press, January 2012. [ bibtex | abstract | DOI | PDF | http ]

[47] Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gómez-Zamalloa, and Germán Puebla. COSTABS: A Cost and Termination Analyzer for ABS. In Oleg Kiselyov and Simon Thompson, editors, Proceedings of the 2012 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23-24, 2012, pages 151-154. ACM Press, 2012. [ bibtex | abstract | DOI ]

[48] Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gómez-Zamalloa, and Germán Puebla. Automatic Inference of Resource Consumption Bounds. In Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings LPAR, volume 7180 of Lecture Notes in Computer Science, pages 1-11. Springer, 2012. [ bibtex | abstract | DOI ]

[49] Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Symbolic Execution of Concurrent Objects in CLP. In Practical Aspects of Declarative Languages (PADL'12), Lecture Notes in Computer Science, pages 123-137. Springer, January 2012. [ bibtex | abstract | DOI | PDF ]

[50] Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Díez. Towards Incremental Resource Usage Analysis. In The Ninth Asian Symposium on Programming Languages and Systems (APLAS'11), December 2011. Poster Presentation. [ bibtex | abstract | PDF ]

[51] Elvira Albert, Israel Cabañas, Antonio Flores-Montoya, Miguel Gómez-Zamalloa, and Sergio Gutiérrez. jPET: an Automatic Test-Case Generator for Java. In 18th Working Conference on Reverse Engineering (WCRE 2011), pages 441-442. IEEE Computer Society, October 2011. [ bibtex | abstract | DOI ]

[52] Elvira Albert, Samir Genaim, Miguel Gómez-Zamalloa, Einar Broch Johnsen, Rudolf Schlatte, and Silvia Lizeth Tapia Tarifa. Simulating Concurrent Behaviors with Worst-Case Cost Bounds. In Michael Butler and Wolfram Schulte, editors, FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings, volume 6664 of Lecture Notes in Computer Science, pages 353-368, 2011. [ bibtex | abstract | DOI ]

[53] Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gómez-Zamalloa, and Germán Puebla. Cost Analysis of Concurrent OO Programs. In Hongseok Yang, editor, Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings, volume 7078 of Lecture Notes in Computer Science, pages 238-254. Springer, 2011. [ bibtex | abstract | DOI ]

[54] Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, and Guillermo Román-Díez. Verified Resource Guarantees using COSTA and KeY. In Siau-Cheng Khoo and Jeremy G. Siek, editors, Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2011, Austin, TX, USA, January 24-25, 2011, SIGPLAN, pages 73-76. ACM, 2011. [ bibtex | abstract | DOI | DOI | PDF ]

[55] Elvira Albert, Samir Genaim, and Abu Naser Masud. More Precise yet Widely Applicable Cost Analysis. In Ranjit Jhala and David A. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, volume 6538 of Lecture Notes in Computer Science, pages 38-53. Springer, January 2011. [ bibtex | abstract | DOI | PDF ]

[56] Elvira Albert, Miguel Gómez-Zamalloa, José Miguel Rojas, and Germán Puebla. Compositional CLP-based Test Data Generation for Imperative Languages. In María Alpuente, editor, LOPSTR 2010 Revised Selected Papers, volume 6564 of Lecture Notes in Computer Science, pages 99-116. Springer-Verlag, 2011. [ bibtex | abstract | DOI | PDF ]

[57] Elvira Albert, Miguel Gómez-Zamalloa, and Germán Puebla. PET: A Partial Evaluation-based Test Case Generation Tool for Java Bytecode. In ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM'10), pages 25-28. ACM Press, 2010. [ bibtex | abstract | PDF ]

[58] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Diana Ramírez-Deantes. From Object Fields to Local Variables: A Practical Approach to Field-Sensitive Analysis. In Radhia Cousot and Matthieu Martel, editors, Static Analysis - 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010. Proceedings, volume 6337 of Lecture Notes in Computer Science, pages 100-116. Springer, 2010. [ bibtex | abstract | DOI | PDF ]

[59] Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gómez-Zamalloa, Germán Puebla, Diana Ramirez, Guillermo Román-Díez, and Damiano Zanardini. Termination and Cost Analysis with COSTA and its User Interfaces. In Spanish Conference on Programming and Computer Languages (PROLE'09), volume 258 of Electronic Notes in Theoretical Computer Science, pages 109-121. Elsevier, September 2009. [ bibtex | abstract | DOI | PDF ]

[60] Elvira Albert, Miguel Gómez-Zamalloa, and Germán Puebla. Test Data Generation of Bytecode by CLP Partial Evaluation. In 18th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'08), number 5438 in Lecture Notes in Computer Science, pages 4-23. Springer-Verlag, March 2009. [ bibtex | abstract | PDF ]
[61] Elvira Albert, Diego Esteban Alonso Blas, Puri Arenas, Samir Genaim, and Germán Puebla. Asymptotic Resource Usage Bounds. In Zhenjiang Hu, editor, Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, volume 5904 of Lecture Notes in Computer Science, pages 294-310. Springer, 2009. [ bibtex | abstract | DOI | PDF | slides ]

[62] Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. Field-Sensitive Value Analysis by Field-Insensitive Analysis. In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM'09, volume 5850 of Lecture Notes in Computer Science, pages 370-386. Springer, 2009. [ bibtex | abstract | DOI | PDF ]

[63] Elvira Albert, Samir Genaim, and Miguel Gómez-Zamalloa. Live heap space analysis for languages with garbage collection. In Hillel Kolodner and Guy L. Steele Jr., editors, Proceedings of the 8th International Symposium on Memory Management, ISMM 2009, Dublin, Ireland, June 19-20, 2009, pages 129-138. ACM, 2009. [ bibtex | abstract | DOI | PDF ]

[64] Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. Cost Relation Systems: a Language-Independent Target Language for Cost Analysis. In Spanish Conference on Programming and Computer Languages (PROLE'08), volume 248 of Electronic Notes in Theoretical Computer Science, pages 31-46. Elsevier, 2009. [ bibtex | abstract | DOI | PDF ]

[65] Miguel Gómez-Zamalloa, Elvira Albert, and Germán Puebla. Modular Decompilation of Low-Level Code by Partial Evaluation. In 8th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM'08), pages 239-248. IEEE Computer Society, September 2008. [ bibtex | abstract | PDF ]
[66] Elvira Albert, John P. Gallagher, Miguel Gómez-Zamalloa, and Germán Puebla. Type-based Homeomorphic Embedding and its Applications to Online Partial Evaluation. In 17th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'07), volume 4915 of Lecture Notes in Computer Science, pages 23-42. Springer-Verlag, February 2008. [ bibtex | abstract | PDF ]
[67] Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In María Alpuente and Germán Vidal, editors, Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings, volume 5079 of Lecture Notes in Computer Science, pages 221-237. Springer, 2008. [ bibtex | abstract | DOI | PDF ]

[68] Elvira Albert, Puri Arenas, Michael Codish, Samir Genaim, Germán Puebla, and Damiano Zanardini. Termination Analysis of Java Bytecode. In Gilles Barthe and Frank S. de Boer, editors, Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings, volume 5051 of Lecture Notes in Computer Science, pages 2-18. Springer, 2008. [ bibtex | abstract | DOI | PDF ]

[69] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. Removing Useless Variables in Cost Analysis of Java Bytecode. In Roger L. Wainwright and Hisham Haddad, editors, Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), Fortaleza, Ceara, Brazil, March 16-20, 2008, pages 368-375. ACM, 2008. [ bibtex | abstract | DOI | PDF ]

[70] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. A Generic Framework for the Cost Analysis of Java Bytecode. In Pimentel Ernesto, editor, Spanish Conference on Programming and Computer Languages (PROLE'07), pages 61-70, September 2007. [ bibtex | abstract | PDF ]

[71] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. Cost Analysis of Java Bytecode. In Rocco De Nicola, editor, Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4421 of Lecture Notes in Computer Science, pages 157-172. Springer-Verlag, March 2007. [ bibtex | abstract | DOI | PDF ]

[72] Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, and Germán Puebla. Verification of Java Bytecode using Analysis and Transformation of Logic Programs. In Ninth International Symposium on Practical Aspects of Declarative Languages (PADL 2007), number 4354 in Lecture Notes in Computer Science, pages 124-139. Springer-Verlag, January 2007. [ bibtex | abstract | PDF ]
[73] Elvira Albert, Samir Genaim, and Miguel Gómez-Zamalloa. Heap Space Analysis for Java Bytecode. In ISMM '07: Proceedings of the 6th International Symposium on Memory Management, pages 105-116, New York, NY, USA, 2007. ACM Press. [ bibtex | abstract | DOI | PDF ]

[74] Elvira Albert, Puri Arenas-Sánchez, Germán Puebla, and Manuel V. Hermenegildo. Reduced Certificates for Abstraction-Carrying Code. In Logic Programming, 22nd International Conference, ICLP 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4079, pages 163-178. Springer, 2006. [ bibtex | abstract | DOI ]

[75] Elvira Albert, Puri Arenas, and Germán Puebla. An Incremental Approach to Abstraction-Carrying Code. In Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, volume 4246, pages 377-391. Springer, 2006. [ bibtex | abstract | DOI ]

[76] Germán Puebla, Elvira Albert, and Manuel V. Hermenegildo. Abstract Interpretation with Specialized Definitions. In Static Analysis, 13th International Symposium, SAS 2006, Seoul, Korea, August 29-31, 2006, Proceedings, volume 4134, pages 107-126. Springer, 2006. [ bibtex | abstract | DOI ]

[77] Germán Puebla, Elvira Albert, and Manuel V. Hermenegildo. A Generic Framework for the Analysis and Specialization of Logic Programs. In Logic Programming, 21st International Conference, ICLP 2005, Sitges, Spain, October 2-5, 2005, Proceedings, pages 407-409. Springer, 2005. [ bibtex | abstract | DOI ]

[78] Elvira Albert, Germán Puebla, and John P. Gallagher. Non-leftmost Unfolding in Partial Evaluation of Logic Programs with Impure Predicates. In Logic Based Program Synthesis and Transformation, 15th International Symposium, LOPSTR 2005, London, UK, September 7-9, 2005, Revised Selected Papers, pages 115-132. Springer, 2005. [ bibtex | abstract | DOI ]

[79] John P. Gallagher, Germán Puebla, and Elvira Albert. Converting One Type-Based Abstract Domain to Another. In Logic Based Program Synthesis and Transformation, 15th International Symposium, LOPSTR 2005, London, UK, September 7-9, 2005, Revised Selected Papers, pages 147-162. Springer, 2005. [ bibtex | abstract | DOI ]

[80] Manuel V. Hermenegildo, Elvira Albert, Pedro López-García, and Germán Puebla. Abstraction carrying code and resource-awareness. In Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 11-13 2005, Lisbon, Portugal, pages 1-11. ACM, 2005. [ bibtex | abstract | DOI ]

[81] Manuel V. Hermenegildo, Elvira Albert, Pedro López-García, and Germán Puebla. Some Techniques for Automated, Resource-Aware Distributed and Mobile Computing in a Multi-paradigm Programming System. In Euro-Par 2004 Parallel Processing, 10th International Euro-Par Conference, Pisa, Italy, August 31-September 3, 2004, Proceedings, volume 3149, pages 21-36. Springer, 2004. [ bibtex | abstract | DOI ]

[82] Elvira Albert, Germán Puebla, and Manuel V. Hermenegildo. Abstract Interpretation-Based Mobile Code Certification. In Logic Programming, 20th International Conference, ICLP 2004, Saint-Malo, France, September 6-10, 2004, Proceedings, pages 446-447. Springer, 2004. [ bibtex | abstract | DOI ]

[83] Germán Puebla, Elvira Albert, and Manuel V. Hermenegildo. Efficient Local Unfolding with Ancestor Stacks for Full Prolog. In Logic Based Program Synthesis and Transformation, 14th International Symposium, LOPSTR 2004, Verona, Italy, August 26-28, 2004, Revised Selected Papers, pages 149-165. Springer, 2004. [ bibtex | abstract | DOI ]

[84] Elvira Albert, Germán Puebla, and Manuel V. Hermenegildo. Abstraction-Carrying Code. In Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, volume 3452, pages 380-397. Springer, 2004. [ bibtex | abstract | DOI ]

[85] Elvira Albert, Germán Puebla, and Manuel V. Hermenegildo. Experiments in abstract interpretation-based code certification for pervasive systems. In Proceedings of the IEEE International Conference on Systems, Man & Cybernetics: The Hague, Netherlands, 10-13 October 2004, pages 1125-1130. IEEE, 2004. [ bibtex | abstract | DOI ]

[86] Elvira Albert, Michael Hanus, and Germán Vidal. A Practical Partial Evaluator for a Multi-Paradigm Declarative Language. In Functional and Logic Programming, 5th International Symposium, FLOPS 2001, Tokyo, Japan, March 7-9, 2001, Proceedings, volume 2024, pages 326-342. Springer, 2001. [ bibtex | abstract | DOI ]

[87] Elvira Albert and Germán Vidal. Symbolic Profiling for Multi-paradigm Declarative Languages. In Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001, Paphos, Cyprus, November 28-30, 2001, Selected Papers, pages 148-167. Springer, 2001. [ bibtex | abstract | DOI ]

[88] Elvira Albert, César Ferri, Frank Steiner, and Germán Vidal. Improving Functional Logic Programs by Difference-Lists. In Advances in Computing Science - ASIAN 2000, 6th Asian Computing Science Conference, Penang, Malaysia, November 25-27, 2000, Proceedings, pages 237-254. Springer, 2000. [ bibtex | abstract | DOI ]

[89] Elvira Albert, Sergio Antoy, and Germán Vidal. Measuring the Effectiveness of Partial Evaluation. In LOPSTR, 2000. [ bibtex | abstract | DOI ]

[90] Elvira Albert, Sergio Antoy, and Germán Vidal. Measuring the Effectiveness of Partial Evaluation in Functional Logic Languages. In Logic Based Program Synthesis and Transformation, 10th International Workshop, LOPSTR 2000 London, UK, July 24-28, 2000, Selected Papers, pages 103-124. Springer, 2000. [ bibtex | abstract | DOI ]

[91] Elvira Albert, Michael Hanus, and Germán Vidal. Using an Abstract Representation to Specialize Functional Logic Programs. In Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings, volume 1955, pages 381-398. Springer, 2000. [ bibtex | abstract | DOI ]

[92] Elvira Albert, María Alpuente, Michael Hanus, and Germán Vidal. A Partial Evaluation Framework for Curry Programs. In Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings, volume 1705, pages 376-395. Springer, 1999. [ bibtex | abstract | DOI ]

[93] Elvira Albert, María Alpuente, Moreno Falaschi, Pascual Julián Iranzo, and Germán Vidal. Improving Control in Functional Logic Program Specialization. In Static Analysis, 5th International Symposium, SAS '98, Pisa, Italy, September 14-16, 1998, Proceedings, pages 262-277. Springer, 1998. [ bibtex | abstract | DOI ]

Publication in Workshops

[1] Elvira Albert, Antonio Flores-Montoya, and Samir Genaim. May-Happen-in-Parallel Analysis with Condition Synchronization. In Foundational and Practical Aspects of Resource Analysis (FOPARA 2015), 2015. [ bibtex | abstract | DOI | PDF | http ]

[2] Elvira Albert, Samir Genaim, and Guillermo Román-Díez. Conditional Termination of Loops over Arrays. In Proceedings of the Bytecode 2012 workshop, the Seventh Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2012), March 2012. [ bibtex | abstract ]

[3] Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, and Guillermo Román-Díez. Verified Resource Guarantees for Heap Manipulating Programs. In 10th KeY Symposium 2011, August 2011. [ bibtex | abstract | PDF ]

[4] Elvira Albert, Puri Arenas, Samir Genaim, Israel Herraiz, and Germán Puebla. Comparing Cost Functions in Resource Analysis. In Marko C. J. D. van Eekelen and Olha Shkaravska, editors, Foundational and Practical Aspects of Resource Analysis - First International Workshop, FOPARA 2009, Eindhoven, The Netherlands, November 6, 2009, Revised Selected Papers, volume 6324 of Lecture Notes in Computer Science, pages 1-17. Springer, 2009. [ bibtex | abstract | DOI | PDF ]

[5] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, Diana Ramírez, and Damiano Zanardini. Upper Bounds of Resource Usage for Java Bytecode using COSTA and its Web Interface. In Workshop on Resource Analysis, September 2008. [ bibtex | abstract | PDF ]

[6] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, Diana Ramírez, and Damiano Zanardini. The COSTA Cost and Termination Analyzer for Java Bytecode and its Web Interface (Tool Demo). In Anna Philippou, editor, 22nd European Conference on Object-Oriented Programming, July 2008. [ bibtex | abstract | PDF ]

[7] Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. Dealing with Numeric Fields in Termination Analysis of Java-like Languages. In 10th Workshop on Formal Techniques for Java-like Programs, July 2008. [ bibtex | abstract | PDF ]

[8] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. COSTA: A Cost and Termination Analyzer for Java Bytecode. In Proceedings of the Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode), Electronic Notes in Theoretical Computer Science, Budapest, Hungary, April 2008. Elsevier. To appear. [ bibtex | abstract | PDF ]

[9] Miguel Gómez-Zamalloa, Elvira Albert, and Germán Puebla. On the Generation of Test Data for Prolog by Partial Evaluation. In Workshop on Logic-based methods in Programming Environments (WLPE'08), pages 26-43, 2008. [ bibtex | abstract | PDF ]
[10] Elvira Albert, Anindya Banerjee, Sophia Drossopoulou, Marieke Huisman, Atsushi Igarashi, Gary T. Leavens, Peter Müller, and Tobias Wrigstad. Formal Techniques for Java-Like Programs. In Object-Oriented Technology. ECOOP 2008 Workshop Reader, ECOOP 2008 Workshops, Paphos, Cyprus, July 7-11, 2008, Final Reports, pages 70-76. Springer, 2008. [ bibtex | abstract | DOI ]

[11] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. Experiments in Cost Analysis of Java Bytecode. In Fausto Spoto and Marieke Huisman, editors, 2nd Workshop on Bytecode Semantics, Verification, Analysis and Transformations, BYTECODE 2007, April 1, 2007, Braga, Portugal, volume 190 of Electronic Notes in Theoretical Computer Science, pages 67-83. Elsevier, April 2007. [ bibtex | abstract | DOI | PDF ]

[12] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. Applications of Static Slicing in Cost Analysis of Java Bytecode. In The 3rd International Workshop on Programming Language Interference and Dependence (PLID'07) ,Kongens Lyngby, Denmark, 21 August, 2007, 2007. [ bibtex | abstract | PDF ]

[13] Elvira Albert, Puri Arenas, Michael Codish, Samir Genaim, Germán Puebla, and Damiano Zanardini. Termination Analysis of Java Bytecode. In Alexander Serebrenik and Dieter Hofbauer, editors, Proceedings of the 9th International Workshop on Termination, WST'07 Paris, France, June 29, 2007, 2007. [ bibtex | abstract | PDF ]

[14] Miguel Gómez-Zamalloa, Elvira Albert, and Germán Puebla. Improving the Decompilation of Java Bytecode to Prolog by Partial Evaluation. Electr. Notes Theor. Comput. Sci., 190(1):85-101, 2007. [ bibtex | abstract | DOI ]

[15] Elvira Albert, Germán Puebla, and Manuel V. Hermenegildo. An Abstract Interpretation-based Approach to Mobile Code Safety. Electr. Notes Theor. Comput. Sci., 132(1):113-129, 2005. [ bibtex | abstract | DOI ]

[16] Germán Puebla, Manuel V. Hermenegildo, and Elvira Albert. A Generic Framework for the Analysis and Specialization of Logic Programs. In Proceedings of the 15th International Workshop on Logic Programming Environments, Sitges (Barcelona), October 5, 2005, pages 61-76, 2005. [ bibtex | abstract | DOI ]

[17] Elvira Albert, Michael Hanus, Frank Huch, Javier Oliver, and Germán Vidal. An Operational Semantics for Declarative Multi-Paradigm Languages. Electr. Notes Theor. Comput. Sci., 70(6):62-83, 2002. [ bibtex | abstract | DOI ]

[18] Elvira Albert, Michael Hanus, Frank Huch, Javier Oliver, and Germán Vidal. Operational Semantics for Functional Logic Languages. Electr. Notes Theor. Comput. Sci., 76:1-19, 2002. [ bibtex | abstract | DOI ]

[19] Elvira Albert, Michael Hanus, and Germán Vidal. Realistic Program Specialization in a Multi-Paradigm Language. In 9th International Workshop on Functional and Logic Programming, WFLP'2000, Benicassim, Spain, September 28-30, 2000, pages 104-119, 2000. [ bibtex | abstract ]

[20] Elvira Albert, Sergio Antoy, and Germán Vidal. A Formal Approach to Reasoning about the Effectiveness of Partial Evaluation. In 9th International Workshop on Functional and Logic Programming, WFLP'2000, Benicassim, Spain, September 28-30, 2000, pages 120-127, 2000. [ bibtex | abstract ]

[21] Elvira Albert, César Ferri, Frank Steiner, and Germán Vidal. List-Processing Optimizations in a Multi-Paradigm Declarative Language. In 9th International Workshop on Functional and Logic Programming, WFLP'2000, Benicassim, Spain, September 28-30, 2000, pages 184-194, 2000. [ bibtex | abstract ]

Books

[1] Elvira Albert, Samir Genaim, Alicia Merayo, and Guillermo Román-Díez. When COSTA Met KeY: Verified Cost Bounds. In Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, and Einar Broch Johnsen, editors, The Logic of Software. A Tasting Menu of Formal Methods - Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday, volume 13360 of Lecture Notes in Computer Science, pages 19-37. Springer, 2022. [ bibtex | abstract | DOI | http ]
[2] Elvira Albert, Jesús Correas, and Guillermo Román-Díez. Resource Analysis of Distributed Systems. In Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, pages 33-46. Springer, 2016. [ bibtex | abstract | DOI | http ]
[3] Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa, and Jose Miguel Rojas. Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency. In Marco Bernardo, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, and Ina Schaefer, editors, Formal Methods for Executable Software Models, volume 8483 of Lecture Notes in Computer Science, pages 263-309. Springer International Publishing, 2014. [ bibtex | abstract | DOI | PDF | http ]

[4] Elvira Albert, Diego Esteban Alonso Blas, Puri Arenas, Jesús Correas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Abu Naser Masud, Germán Puebla, José Miguel Rojas, Guillermo Román-Díez, and Damiano Zanardini. Automatic Inference of Bounds on Resource Consumption. In Formal Methods for Components and Objects - 11th International Symposium, FMCO 2012, Bertinoro, Italy, September 24-28, 2012, Revised Lectures, volume 7866 of Lecture Notes in Computer Science, pages 119-144. Springer, 2013. [ bibtex | abstract | DOI | PDF | http ]

[5] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. Resource Usage Analysis and its Application to Resource Certification. In Alessandro Aldini, Gilles Barthe, and Roberto Gorrieri, editors, Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, volume 5705 of Lecture Notes in Computer Science, pages 258-288. Springer, 2009. [ bibtex | abstract | DOI | PDF ]

[6] Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, Formal Methods for Components and Objects, 6th International Symposium, FMCO 2007, Amsterdam, The Netherlands, October 24-26, 2007, Revised Lectures, volume 5382 of Lecture Notes in Computer Science, pages 113-132. Springer, 2008. [ bibtex | abstract | DOI | PDF ]

Quick Links

Recent News