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

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

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

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

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

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

[5] 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 ]
[6] 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] 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, January 2016. [ bibtex | abstract | DOI | PDF ]

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

[3] 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):173-199, 2016. [ bibtex | abstract | DOI | PDF ]
[4] 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 ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[26] 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 ]
[27] 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 ]
[28] 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. To appear. [ bibtex | abstract | PDF ]

[29] 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. [ bibtex | abstract | DOI | PDF | http ]

Conference Publications

[1] 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 ]
[2] Elvira Albert, Nikolaos Bezirgiannis, Frank de Boer, and Enrique Martin-Martin. A Formal, Resource Consumption-Preserving Translation of Actors to Haskell. In Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016, Lecture Notes in Computer Science. Springer, 2016. To appear. [ bibtex | abstract ]
[3] Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. Combining Static Analysis and Testing for Deadlock Detection. In 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 | PDF ]

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

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

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

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

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

[10] Elvira Albert, Samir Genaim, and Pablo Gordillo. May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. In 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 ]

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

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

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

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

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

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

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

[18] Elvira Albert, Samir Genaim, and Raúl Gutiérrez. Towards a Transformational Approach to Resource Analysis with Typed-Norms (Extended Abstract). In 23rd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'13), pages 85-96, September 2013. [ bibtex | abstract | PDF ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[19] 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] E. Albert, M. Gómez-Zamalloa, and M. Isabel. Combining Static Analysis and Testing for Deadlock Detection. Technical report, 2015. [ bibtex | abstract | PDF ]

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

Quick Links