This is a list of COSTA related papers, classified into categories and in reverse chronological order inside each category. Please note the following copyright notice: The documents distributed have been provided by the contributing authors as a means to ensure timely dissemination of technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Book Chapters

[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 ]

Books Edited

[1] Elvira Albert and Laura Kovács, editors. LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing. EasyChair, 2020. [ bibtex | abstract | http ]
[2] Elvira Albert, Ivan Lanese, Alberto Lluch Lafuente, and José Proença. Selected Papers of the Conferences FORTE and COORDINATION 2016. Logical Methods in Computer Science, 2018. [ bibtex | abstract | http ]
[3] Elvira Albert and Ivan Lanese, editors. Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings, volume 9688 of Lecture Notes in Computer Science. Springer, 2016. [ bibtex | abstract | DOI | http ]
[4] Elvira Albert and Shin-Cheng Mu. Selected and extended papers from Partial Evaluation and Program Manipulation 2013. Sci. Comput. Program., 95:147-148, 2014. [ bibtex | abstract | DOI | http ]
[5] Elvira Albert and Emil Sekerinski, editors. Integrated Formal Methods - 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings, volume 8739 of Lecture Notes in Computer Science. Springer, 2014. [ bibtex | abstract | DOI | http ]
[6] Miguel Gómez-Zamalloa and Germán Puebla, editors. Special Section: ACM SAC-SVT 2013 + Bytecode 2013, Science of Computer Programming. Elsevier - North Holland, 2014. [ bibtex | abstract | http ]
[7] Elvira Albert and Shin-Cheng Mu, editors. Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, Rome, Italy, January 21-22, 2013. ACM, 2013. [ bibtex | abstract | http ]

[8] Elvira Albert, editor. Logic-Based Program Synthesis and Transformation, 22nd International Symposium, LOPSTR 2012, Leuven, Belgium, September 18-20, 2012, Revised Selected Papers, volume 7844 of Lecture Notes in Computer Science. Springer, 2013. [ bibtex | abstract | http ]

[9] Puri Arenas and Víctor M. Gulías, editors. Proceedings of the XI Spanish Conference on Programming and Languages, PROLE 2011, volume 282. Elsevier, 2012. [ bibtex | abstract | DOI ]

[10] Elvira Albert and Samir Genaim, editors. Proceedings of the Workshop on Bytecode Semantics, Verification, Analysis and Transformation, Electronic Notes in Theoretical Computer Science. Elsevier - North Holland, 2009. [ bibtex | abstract | DOI ]
[11] Sergio Antoy and Elvira Albert, editors. Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 15-17, 2008, Valencia, Spain. ACM, 2008. [ bibtex | abstract ]

Journal Publications

[1] Shankara Pailoor, Yanju Chen, Franklyn Wang, Clara Rodríguez-Núñez, Jacob Van Geffen, Jason Morton, Michael Chu, Brian Gu, Yu Feng, and Isil Dillig. Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs. Proc. ACM Program. Lang., 7(PLDI):1510-1532, 2023. [ bibtex | abstract | DOI | http ]

[2] Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, and Mooly Sagiv. Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. IEEE Trans. Dependable Secur. Comput., 20(3):2256-2273, 2023. [ bibtex | abstract | DOI | http ]

[3] Elvira Albert, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, Miguel Isabel, and Peter J. Stuckey. Optimal dynamic partial order reduction with context-sensitive independence and observers. Journal of Systems and Software, 202:111730, 2023. [ bibtex | abstract | DOI | http ]

[4] 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 ]

[5] 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 ]

[6] Jesús Correas, Pablo Gordillo, and Guillermo Román-Díez. Static Profiling and Optimization of Ethereum Smart Contracts Using Resource Analysis. IEEE Access, 9:25495-25507, 2021. [ bibtex | abstract | DOI | http ]
[7] Miguel Gómez-Zamalloa and Miguel Isabel. Deadlock-Guided Testing. IEEE Access, 9:46033-46048, 2021. [ bibtex | abstract | DOI | http ]
[8] 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 ]

[9] 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 ]
[10] 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 ]
[11] Jesús J. Doménech, John P. Gallagher, and Samir Genaim. Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis. Theory and Practica of Logic Programming, 19(5-6):990-1005, 2019. [ bibtex | abstract | DOI ]

[12] 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 ]
[13] Cosimo Laneve, Michael Lienhardt, Ka I Pun, and Guillermo Román-Díez. Time analysis of actor programs. Journal of Logical and Algebraic Methods in Programming, 105:1 - 27, 2019. [ bibtex | abstract | DOI ]

[14] 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 ]

[15] 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 ]

[16] Damiano Zanardini. Field-sensitive sharing. Journal of Logical and Algebraic Methods in Programming, 95:103-127, 2018. [ bibtex | abstract | DOI | http ]
[17] Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Systematic testing of actor systems. Software Testing, Verification and Reliability, 2018. [ bibtex | abstract | DOI | http ]

[18] Jesús Correas, Sonia Estévez Martín, and Fernando Sáenz-Pérez. Enhancing set constraint solvers with bound consistency. Expert Systems with Applications, 92:485-494, 2018. [ bibtex | abstract | DOI | http ]

[19] Isabela Mastroeni and Damiano Zanardini. Abstract Program Slicing: an Abstract Interpretation-based approach to Program Slicing. ACM Transactions on Computational Logic, 18(1):7:1-7:58, 2017. [ bibtex | abstract | DOI | http ]
[20] 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 ]

[21] 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 ]

[22] 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 ]

[23] 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 ]

[24] 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 ]

[25] 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 ]

[26] 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 ]

[27] Peter Y.H. Wong, Richard Bubel, Frank S. de Boer, Miguel Gómez-Zamalloa, Stijn de Gouw, Renier Hahnle, Karl Meinke, and MuddassarAzam Sindhu. Testing Abstract Behavioral Specifications. International Journal on Software Tools for Technology Transfer, 17(1):107-119, Feb 2015. [ bibtex | abstract | DOI | PDF | http ]
[28] 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 ]

[29] Damiano Zanardini and Samir Genaim. Inference of Field-Sensitive Reachability and Cyclicity. ACM Transactions on Computational Logic, 15(4):33:1-33:41, September 2014. [ bibtex | abstract | DOI | arXiv | http ]

[30] Amir M. Ben-Amram and Samir Genaim. Ranking Functions for Linear-Constraint Loops. Journal of the ACM, 61(4):26, 2014. [ bibtex | abstract | arXiv | DOI | http ]

[31] 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 ]

[32] 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 ]

[33] 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 ]

[34] Samir Genaim and Damiano Zanardini. Reachability-based Acyclicity Analysis by Abstract Interpretation. Theoretical Computer Science, 474(0):60 - 79, 2013. Los agradecimientos al proyecto se han publicado en: Corrigendum to “Reachability-based acyclicity analysis by abstract interpretation” [Theoretical Computer Science 474 (2013) 60-79]. Theoretical Computer Science, 503(0):115, 2013. [ bibtex | abstract | DOI | PDF | http ]

[35] 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 ]

[36] 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 ]

[37] Damiano Zanardini. Class-level Non-Interference. New Generation Computing, 30(2-3):241-270, 2012. [ bibtex | abstract | PDF ]

[38] Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the Termination of Integer Loops. ACM Trans. Program. Lang. Syst., 34(4):16, 2012. [ bibtex | abstract | DOI | PDF ]

[39] 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 ]

[40] 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 ]

[41] 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 ]

[42] 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 ]

[43] 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 ]

[44] 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 ]

[45] 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 ]
[46] 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 ]

Conference Publications

[1] Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Albert Rubio. Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT. In ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2024. Proceedings, ACM, 2024. To appear. [ bibtex | abstract ]

[2] Elvira Albert, Maria Garcia de la Banda, Alejandro Hernández-Cerezo, Alexey Ignatiev, Albert Rubio, and Peter J. Stuckey. SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-based, and SAT Techniques. In PLDI '24: 45th ACM SIGPLAN International Conference on Programming Language Design and Implementation, Copenhagen, Denmark, June 24-28, 2024. ACM, 2024. [ bibtex | abstract ]

[3] M. Isabel, C. Rodríguez-Núñez, and A. Rubio. Scalable Verification of Zero-Knowledge Protocols. In 2024 IEEE Symposium on Security and Privacy (SP), pages 132-132, Los Alamitos, CA, USA, 2024. IEEE Computer Society. [ bibtex | abstract | DOI | http ]

[4] Elvira Albert, Samir Genaim, Daniel Kirchner, and Enrique Martin-Martin. Formally Verified EVM Block-Optimizations. In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 of Lecture Notes in Computer Science, pages 176-189. Springer, 2023. [ bibtex | abstract | DOI ]
[5] 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, volume 13993 of Lecture Notes in Computer Science, pages 448-466. Springer, 2023. [ bibtex | abstract | DOI | PDF ]

[6] 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 ]

[7] 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 ]
[8] 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 ]

[9] Elvira Albert, Samir Genaim, Enrique Martin-Martin, 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 ]

[10] 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 ]

[11] 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, pages 209:1-209:30, 2020. [ bibtex | abstract | DOI ]

[12] 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 ]

[13] 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 ]

[14] 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 ]
[15] Amir M. Ben-Amram, Jesús J. Doménech, and Samir Genaim. Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets. In Bor-Yuh Evan Chang, editor, Proceedings of the 26th International Symposium on Static Analysis (SAS'19), volume 11822 of Lecture Notes in Computer Science, pages 459-480. Springer, 2019. [ bibtex | abstract | DOI ]

[16] 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 ]

[17] 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 ]
[18] Miguel Isabel. Conditional Dynamic Partial Order Reduction and Optimality Results. In Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis 2019 (ISSTA'19), ACM, 2019. [ bibtex | abstract | DOI | PDF ]
[19] 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 ]

[20] 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 ]

[21] 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 ]
[22] 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 ]
[23] 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 ]
[24] 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 ]
[25] Amir M. Ben-Amram and Samir Genaim. On Multiphase-Linear Ranking Functions. In Viktor Kuncak and Rupak Majumdar, editors, Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17), volume 10427 of Lecture Notes in Computer Science, pages 601-620. Springer, 2017. [ bibtex | abstract | DOI ]

[26] 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 ]
[27] 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 ]

[28] Jesús J. Doménech, Samir Genaim, Einar Broch Johnsen, and Rudolf Schlatte. EasyInterface: A toolkit for rapid development of GUIs for research prototype tools. In Fundamental Approaches to Software Engineering: 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Lecture Notes in Computer Science, pages 379-383. Springer, 2017. [ bibtex | abstract | DOI | http ]

[29] 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 ]
[30] 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 ]
[31] 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 ]

[32] 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 ]

[33] Amir M. Ben-Amram and Samir Genaim. Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions. In Daniel Kroening and Corina S. Pasareanu, editors, 27th International Conference on Computer Aided Verification (CAV 2015), volume 9207 of Lecture Notes in Computer Science, pages 304-321. Springer, July 2015. [ bibtex | abstract | DOI | arXiv | PDF | http ]

[34] L. Bozzelli and D. Pearce. On the Complexity of Temporal Equilibrium Logic. In Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on, pages 645-656, 2015. [ bibtex | abstract | DOI | http ]

[35] Pierre Ganty, Samir Genaim, Ratan Lal, and Pavithra Prabhakar. From Non-Zenoness Verification to Termination. In Proceedings of the 13th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE'15, pages 228-237. IEEE, 2015. [ bibtex | abstract | DOI | PDF | http ]

[36] 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 ]
[37] 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 ]

[38] 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 ]

[39] 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 ]

[40] 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 ]

[41] 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 ]

[42] 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 ]

[43] 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 ]

[44] 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 ]

[45] 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 ]

[46] 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 ]

[47] Pierre Ganty and Samir Genaim. Proving Termination Starting from the End. In Natasha Sharygina and Helmut Veith, editors, 25th International Conference on Computer Aided Verification (CAV 2013), volume 8044 of Lecture Notes in Computer Science, pages 397-412. Springer, July 2013. [ bibtex | abstract | DOI | http ]

[48] 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 ]

[49] 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 ]

[50] 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 ]

[51] 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 ]

[52] Diego Esteban Alonso Blas, Puri Arenas, and Samir Genaim. Precise Cost Analysis via Local Reasoning. 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 319-333. Springer, 2013. [ bibtex | abstract | DOI | PDF | http ]

[53] Amir M. Ben-Amram and Samir Genaim. On the Linear Ranking Problem for Integer Linear-Constraint Loops. In Roberto Giacobazzi and Radhia Cousot, editors, 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), pages 51-62. ACM Press, January 2013. [ bibtex | abstract | DOI | http ]

[54] José Miguel Rojas and Miguel Gómez-Zamalloa. A Framework for Guided Test Case Generation in Constraint Logic Programming. In LOPSTR 2012, volume 7844 of Lecture Notes in Computer Science, pages 176-193. Springer, 2013. [ bibtex | abstract | DOI | PDF | http ]

[55] 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 ]

[56] Diego Esteban Alonso Blas and Samir Genaim. On the Limits of the Classical Approach to Cost Analysis. In Antoine Miné and David Schmidt, editors, Static Analysis - 19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012. Proceedings, volume 7460 of Lecture Notes in Computer Science, pages 405-421. Springer, September 2012. [ bibtex | abstract | DOI | PDF | slides ]

[57] 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 ]

[58] 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 ]

[59] 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 ]

[60] Sonia Estévez-Martín, Jesús Correas-Fernández, and Fernando Sáenz-Pérez. Extending the TOY System with the ECLIPSE Solver over Sets of Integers. In FLOPS'12, volume 7294 of Lecture Notes in Computer Science, pages 120-135. Springer, 2012. [ bibtex | abstract | PDF ]

[61] 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 ]

[62] 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 ]

[63] 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 ]

[64] 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 ]

[65] 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 ]

[66] 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 ]

[67] Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the Termination of Integer Loops. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, USA, January 25-27, 2012. Proceedings, volume 7148 of Lecture Notes in Computer Science, pages 72-87. Springer, January 2012. [ bibtex | abstract | DOI | PDF ]

[68] Diana Ramírez-Deantes, Jesús Correas, and Germán Puebla. Modular Termination Analysis of Java Bytecode and its Application to phoneME Core Libraries. In Formal Aspects of Computer Software (FACS 2010), volume 6921 of Lecture Notes in Computer Science, pages 218-236. Springer, 2012. [ bibtex | abstract ]

[69] 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 ]

[70] 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 ]

[71] 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 ]

[72] 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 ]

[73] 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 ]

[74] 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 ]

[75] 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 ]

[76] 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 ]

[77] 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 ]

[78] 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 ]

[79] 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 ]
[80] 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 ]

[81] 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 ]

[82] 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 ]

[83] 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 ]

[84] 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 ]
[85] 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 ]
[86] 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 ]

[87] 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 ]

[88] 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 ]

[89] 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 ]

[90] 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 ]

[91] 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 ]
[92] 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 ]

Ph.D. Dissertations

[1] Clara Rodríguez-Núñez. Safety and Security Properties in Blockchain Technologies. PhD thesis, Facultad de Informática, Universidad Complutense de Madrid (Complutense University of Madrid), 2023. [ bibtex | abstract ]

[2] Alicia Merayo. Resource Analysis of Integer and Abstract Programs. PhD thesis, Facultad de Informática, Universidad Complutense de Madrid (Complutense University of Madrid), May 2022. [ bibtex | abstract ]

[3] Jesús J. Doménech. Termination Analysis of Programs with Complex Control-Flow. PhD thesis, Facultad de Informática, Universidad Complutense de Madrid (Complutense University of Madrid), February 2021. [ bibtex | abstract | PDF ]

[4] Miguel Isabel. Verification of Concurrent Systems: Optimality, Scalability and Applicability. PhD thesis, Facultad de Informática, Universidad Complutense de Madrid (Complutense University of Madrid), October 2020. [ bibtex | abstract | PDF ]

[5] Pablo Gordillo. Static Analysis of Concurrent and Distributed Systems: Concurrent Objects and Ethereum Bytecode. PhD thesis, Facultad de Informática, Universidad Complutense de Madrid (Complutense University of Madrid), January 2020. [ bibtex | abstract | PDF ]

[6] Diego Esteban Alonso Blas. From Abstract Programs to Precise Asymptotic Closed-Form Bounds. PhD thesis, Facultad de Informática, Universidad Complutense de Madrid (Complutense University of Madrid), May 2014. [ bibtex | abstract | PDF | http ]

[7] José Miguel Rojas. Test Case Generation in Object-Oriented Programming. PhD thesis, Facultad de Informática, Universidad Politécnica de Madrid (Technical University of Madrid), December 2013. [ bibtex | abstract | DOI | http ]
[8] Md. Abu Naser Masud. Termination and Cost Analysis: Complexity and Precision Issues. PhD thesis, Facultad de Informática, Universidad Politécnica de Madrid (Technical University of Madrid), February 2013. [ bibtex | abstract | PDF | http ]

[9] Guillermo Román-Díez. Advanced Topics in Resource Analysis: Certification, Incrementality, Concurrency and Array-sensitivity. PhD thesis, Facultad de Informática, Universidad Politécnica de Madrid (Technical University of Madrid), December 2012. [ bibtex | abstract | PDF ]

[10] Diana Ramírez-Deantes. Modular and Field-Sensitive Termination Analysis of Java Bytecode. PhD thesis, Facultad de Informática, Universidad Politécnica de Madrid (Technical University of Madrid), February 2011. [ bibtex | abstract | PDF ]

[11] Miguel Gómez-Zamalloa. Transformation and Analysis of Object-Oriented Bytecode. PhD thesis, Facultad de Informática, Universidad Complutense de Madrid (Complutense University of Madrid), July 2009. [ bibtex | abstract | PDF ]

Workshop Publications

[1] Jesús J. Doménech and Samir Genaim. Termination Analysis of Programs with Multiphase Control-Flow. In Hossein Hojjat and Bishoksan Kafle, editors, Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS'21), pages 13-21, 2021. [ bibtex | abstract | DOI ]

[2] Amir M. Ben-Amram, Jesús J. Doménech, and Samir Genaim. Loops for which Multiphase-Linear Ranking Functions are Sufficient. In Samir Genaim, editor, Proceedings of the 17th International Workshop on Termination (WST'21), pages 60-74, 2021. [ bibtex | abstract ]

[3] Alicia Merayo and Samir Genaim. Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations. In Salvador Lucas, editor, Proceedings of the 16th International Workshop on Termination, WST'18 Oxford, pages 60-64, 2018. [ bibtex | abstract | PDF | slides ]
[4] Jesús J. Doménech, Samir Genaim, and John P. Gallagher. Control-Flow Refinement via Partial Evaluation. In Salvador Lucas, editor, Proceedings of the 16th International Workshop on Termination, WST'18 Oxford, page 55, 2018. [ bibtex | abstract | PDF | slides ]

[5] 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 ]

[6] José Miguel Rojas and Corina S. Pāsāreanu. Compositional Symbolic Execution through Program Specialization. In BYTECODE 2013, 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation, March 2013. [ bibtex | abstract | PDF | .pdf ]

[7] Karina Villela, Taslim Arif, and Damiano Zanardini. Towards Product Configuration Taking into Account Quality Concerns. In Workshop on Formal Methods and Analysis in Software Product Line Engineering (FMSPLE). In Proceedings of SPLC, Volume 2, pages 82-90. ACM Press, September 2012. [ bibtex | abstract ]

[8] 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 ]

[9] 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 ]

[10] Diego Esteban Alonso Blas, Puri Arenas, and Samir Genaim. Handling Non-linear Operations in the Value Analysis of COSTA. In Proceedings of the Bytecode 2011 workshop, the Sixth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode), volume 279 Issue 1 of Electronic Notes in Theoretical Computer Science, pages 3-17. Elsevier, 2011. [ bibtex | abstract | DOI | PDF | slides ]

[11] Samir Genaim and Damiano Zanardini. The Acyclicity Inference of COSTA. In 11th International Workshop on Termination, July 2010. [ bibtex | abstract | PDF ]

[12] Dave Clarke, Nikolay Diakov Reiner Hähnle, Einar Broch Johnsen, Germán Puebla, Balthasar Weitzel, and Peter Y. H. Wong. HATS-A Formal Software Product Line Engineering Methodology. In 1st International Workshop on Formal Methods in Software Product Line Engineering, 2010. [ bibtex | abstract | PDF ]

[13] 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 ]

[14] 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 ]

[15] 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 ]

[16] Samir Genaim and Fausto Spoto. Constancy Analysis. In 10th Workshop on Formal Techniques for Java-like Programs, July 2008. [ bibtex | abstract | PDF ]

[17] 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 ]

[18] 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 ]

[19] 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 ]
[20] 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 ]

[21] 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 ]

[22] 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 ]

[23] 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 ]

Newsletter

[1] 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. Resource Analysis in the COSTA System. December 2012. Newsletter. [ bibtex | abstract | PDF | http ]

Technical Reports

[1] Elvira Albert, Jesús Correas, Pablo Gordillo, Alejandro Hernández-Cerezo, Guillermo Román-Díez, and Albert Rubio. Analyzing Smart Contracts: From EVM to a Sound Control-Flow Graph. Technical report, 2020. [ bibtex | abstract | PDF ]
[2] Elvira Albert, Miguel Gómez-Zamalloa, Albert Rubio, Matteo Sammartino, and Alexandra Silva. SDN-Actors: Modeling and Verification of SDN Programs (Technical report). Technical report, 2018. [ bibtex | abstract | PDF ]
[3] E. Albert, M. Gómez-Zamalloa, and M. Isabel. Deadlock Guided Testing in CLP. Technical report, 2017. [ bibtex | abstract | PDF ]

[4] E. Albert, M. Gómez-Zamalloa, and M. Isabel. Combining Static Analysis and Testing for Deadlock Detection. Technical report, 2015. [ bibtex | abstract | PDF ]

[5] Samir Genaim and Damiano Zanardini. Automatic Inference of Acyclicity. Technical report, 2010. [ bibtex | abstract | PDF ]

Quick Links