Static analysis which takes into account the values of data stored in the heap is considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields nor of array contents, i.e., they are heap-insensitive. In this article, we propose locality conditions for soundly tracking heap-allocated data in Java (bytecode) programs, by means of ghost non-heap allocated variables. This way, heap-insensitive analysis over the transformed program can infer information on the original heap-allocated data without sacrificing efficiency. If the locality conditions cannot be proven unconditionally, we seek to generate aliasing preconditions which, when they hold in the initial state, guarantee the termination of the program. Experimental results show that we greatly improve the accuracy w.r.t. a heap-insensitive analysis while the overhead introduced is reasonable.

@article{AlbertAGPG13,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ\'{a}n Puebla and Guillermo Rom\'{a}n-D\'{i}ez},
  title = {{C}onditional {T}ermination of {L}oops over {H}eap-allocated {D}ata},
  journal = {Science of Computer Programming},
  year = {2013},
  publisher = {Elsevier},
  note = {To Appear}
}

Cost analysis statically approximates the cost of programs in terms of their input data size. This paper presents, to the best of our knowledge, the first approach to the automatic cost analysis of Object-Oriented bytecode programs. In languages such as Java and C#, analyzing bytecode has a much wider application area than analyzing source code since the latter is often not available. Cost analysis in this context has to consider, among others, dynamic dispatch, jumps, the operand stack, and the heap. Our method takes a bytecode program and a cost model specifying the resource of interest, and generates cost relations which approximate the execution cost of the program with respect to such resource. We report on COSTA, an implementation for Java bytecode which can obtain upper bounds on cost for a large class of programs and complexity classes. Our basic techniques can be directly applied to infer cost relations for other Object-Oriented imperative languages, not necessarily in bytecode form.

@article{AlbertAGPZ12,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Damiano Zanardini},
  title = {Cost {A}nalysis of {O}bject-{O}riented {B}ytecode {P}rograms},
  journal = {Theoretical Computer Science (Special Issue on Quantitative Aspects of Programming Languages)},
  volume = 413,
  number = 1,
  pages = {142--159},
  year = {2012},
  publisher = {Elsevier},
  issn = {0304-3975},
  doi = {10.1016/j.tcs.2011.07.009},
  url = {http://www.sciencedirect.com/science/article/pii/S0304397511006190}
}

@article{hermenegildo11:ciao-design-tplp,
  author = {M. V. Hermenegildo and F. Bueno and M. Carro and 
                  P. L\'{o}pez and E. Mera and J.F. Morales and Germ\'an Puebla},
  title = {{A}n {O}verview of {C}iao and its {D}esign {P}hilosophy},
  journal = {Theory and Practice of Logic Programming},
  year = {2012},
  month = {January},
  volume = {12},
  number = {1--2},
  pages = {219--252},
  publisher = {Cambridge University Press},
  projects = {HATS,PROMETIDOS,DOVES,SCUBE,POAIST},
  butopics = {lang,impl,autop,debug,env,anal,spec,gran},
  doi = {doi:10.1017/S1471068411000457},
  note = {http://arxiv.org/abs/1102.5497}
}

@article{ai-safety-reduced-tplp,
  author = {Elvira Albert and Puri Arenas and Germ\'an Puebla and M. Hermenegildo},
  title = {{C}ertificate {S}ize {R}eduction in {A}bstraction-{C}arrying {C}ode},
  journal = {Theory and Practice of Logic Programming},
  year = 2012,
  projects = {HATS,DOVES,PROMETIDOS},
  butopics = {anal,debug},
  buconfj = {tplp}
}

The classical approach to automatic cost analysis consists of two phases. Given a program and some measure of cost, the analysis first produces cost relations (CRs), i.e., recursive equations which capture the cost of the program in terms of the size of its input data. Second, CRs are converted into closed-form, i.e., without recurrences. Whereas the first phase has received considerable attention, with a number of cost analyses available for a variety of programming languages, the second phase has been comparatively less studied. This article presents, to our knowledge, the first practical framework for the generation of closed-form upper bounds for CRs which (1) is fully automatic, (2) can handle the distinctive features of CRs originating from cost analysis of realistic programming languages, (3) is not restricted to simple complexity classes, and (4) produces reasonably accurate solutions. A key idea in our approach is to view CRs as programs, which allows applying semantic-based static analyses and transformations to bound them, namely our method is based on the inference of ranking functions and loop invariants and on the use of partial evaluation.

@article{AlbertAGP11a,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ\'an Puebla},
  title = {{C}losed-{F}orm {U}pper {B}ounds in {S}tatic {C}ost {A}nalysis},
  journal = {Journal of Automated Reasoning},
  year = {2011},
  month = {February},
  publisher = {Springer},
  volume = {46},
  number = {2},
  pages = {161-203},
  issn = {0168-7433}
}

@article{tplp-unfolding,
  author = {Germ\'an Puebla and Elvira Albert and M.~Hermenegildo},
  title = {Efficient {L}ocal {U}nfolding with {A}ncestor {S}tacks},
  journal = {Theory and Practice of Logic Programming},
  year = {2011},
  pages = {1--32},
  volume = 11,
  month = {January},
  number = 1,
  butopics = {spec},
  buconfj = {tplp},
  projects = {HATS,SCUBE,DOVES,PROMESAS},
  publisher = {Cambridge U. Press},
  publisher_location = {U.K.},
  issn = {1471-0684}
}

@article{Gomez-ZAP10,
  author = {Miguel G\'{o}mez-Zamalloa and Elvira Albert and Germ{\'a}n Puebla},
  title = {{T}est {C}ase {G}eneration for {O}bject-{O}riented {I}mperative {L}anguages in {CLP}},
  journal = {Theory and Practice of Logic Programming, 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue},
  year = {2010},
  month = {July},
  editor = {M.~Hermenegildo and T.~Schaub},
  pages = {659--674},
  volume = {10},
  number = {4-6},
  issn = {1471-0684},
  publisher = {Cambridge U. Press}
}

@article{Gomez-ZAP09,
  author = {Miguel G\'{o}mez-Zamalloa and Elvira Albert and Germ{\'a}n Puebla},
  title = {{D}ecompilation of {J}ava {B}ytecode to {P}rolog by {P}artial {E}valuation},
  journal = {Information and Software Technology},
  publisher = {Elsevier},
  volume = {51},
  number = {10},
  issn = {0950-5849},
  pages = {1409--1427},
  npages = {19},
  month = {October},
  year = {2009}
}

@article{AlbertGGP09,
  author = {Elvira Albert and John P. Gallagher and Miguel G\'{o}mez-Zamalloa and Germ{\'a}n Puebla},
  title = {{T}ype-based {H}omeomorphic {E}mbedding for {O}nline {T}ermination},
  journal = {Information Processing Letters},
  publisher = {Elsevier},
  volume = {109},
  number = {15},
  issn = {0020-0190},
  pages = {879--886},
  month = {July},
  year = {2009}
}

@article{ai-safety-ngc07,
  author = {Elvira Albert and Germ\'an Puebla and M.~Hermenegildo},
  title = {Abstraction-{C}arrying {C}ode: {A} {M}odel for {M}obile
                  {C}ode {S}afety},
  year = 2008,
  month = {March},
  volume = 26,
  number = 2,
  pages = {171--204},
  projects = {MOBIUS,MERIT,PROMESAS,POAIST},
  butopics = {anal,debug},
  buconfj = {ngc},
  journal = {New Generation Computing}
}

@article{ciaopp-sas03-journal-scp,
  author = {M.~Hermenegildo and Germ\'an Puebla and F.~Bueno and
                  P.~L\'{o}pez-Garc\'{\i}a},
  title = {{I}ntegrated {P}rogram {D}ebugging, {V}erification, and
                  {O}ptimization {U}sing {A}bstract {I}nterpretation
                  (and {T}he {C}iao {S}ystem {P}reprocessor)},
  journal = {Science of Computer Programming},
  year = 2005,
  volume = 58,
  number = {1--2},
  npages = 31,
  pages = {115--140},
  buconfj = {scp},
  publisher = {Elsevier Science},
  publisher_location = {Amsterdam, Holland},
  butopics = {anal,spec,autop,gran,debug,impl,env},
  projects = {ASAP,CUBICO,POAIST},
  issn = {ISSN 0167-6423}
}

@article{incanal-toplas,
  author = {M.~Hermenegildo and Germ\'an Puebla and K.~Marriott and
                  P.~Stuckey},
  title = {{I}ncremental {A}nalysis of {C}onstraint {L}ogic
                  {P}rograms},
  journal = {ACM Transactions on Programming Languages and Systems},
  publisher = {ACM Press},
  year = 2000,
  month = {March},
  volume = 22,
  number = 2,
  pages = {187--223},
  butopics = {anal,cons},
  buconfj = {toplas},
  projects = {EDIPIA}
}

@article{spec-jlp,
  author = {Germ\'an Puebla and M.~Hermenegildo},
  title = {{A}bstract {M}ultiple {S}pecialization and its
                  {A}pplication to {P}rogram {P}arallelization},
  journal = {J.~of Logic Programming. Special Issue on Synthesis,
                  Transformation and Analysis of Logic Programs},
  year = 1999,
  volume = 41,
  number = {2\&3},
  pages = {279--316},
  month = {November},
  publisher = {{E}lsevier - {N}orth {H}olland},
  publisher_location = {NY, USA},
  npages = 38,
  butopics = {autop,spec,anal},
  buconfj = {jlp},
  projects = {DISCIPL, ELLA}
}

When reasoning about distributed systems, it is essential to have information about the different kinds of nodes which compose the system, how many instances of each kind exist, and how nodes communicate with other nodes. In this paper we present a static-analysis-based approach which is able to provide information about the questions above. In order to cope with an unbounded number of nodes and an unbounded number of calls among them, the analysis performs an abstraction of the system producing a graph whose nodes may represent (infinitely) many concrete nodes and arcs represent any number of (infinitely) many calls among nodes. The crux of our approach is that the abstraction is enriched with upper bounds inferred by a resource analysis which limit the number of concrete instances which the nodes and arcs represent. The combined information provided by our approach has interesting applications such as debugging, optimizing and dimensioning distributed systems.

@inproceedings{AlbertCPR13,
  author = {Elvira Albert and Jes\'us Correas and Germ\'an Puebla and Guillermo Rom\'an-D\'iez},
  title = {{Q}uantified {A}bstractions of {D}istributed {S}ystems},
  booktitle = {10th International Conference on integrated Formal Methods (iFM'13)},
  year = {2013},
  month = {June},
  note = {To appear}
}

The aim of incremental global analysis is, given a program, its analysis results and a series of changes to the program, to obtain the new analysis results as efficiently as possible and, ideally, without having to (re-)analyze fragments of code which are not affected by the changes. Incremental analysis can significantly reduce both the time and the memory requirements of analysis. This paper presents an incremental resource usage (a.k.a. cost) analysis for a sequential Java-like language. Our main contributions are (1) a multi-domain incremental fixed-point algorithm which can be used by all global (pre-)analyses required to infer the cost (including class, sharing, cyclicity, constancy, and size analyses) and which takes care of propagating dependencies among such domains, and (2) a novel form of cost summaries which allows us to incrementally reconstruct only those components of cost functions affected by the change. Experimental results in the COSTA system show that the proposed incremental analysis can perform very efficiently in practice.

@inproceedings{AlbertCPR12,
  author = {Elvira Albert and Jes\'us Correas and Germ\'an Puebla and Guillermo Rom\'an-D\'iez},
  title = {{I}ncremental {R}esource {U}sage {A}nalysis},
  booktitle = {Proceedings of the 2012 ACM SIGPLAN Workshop on Partial
               Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, 
               January 23-24, 2012},
  publisher = {ACM Press},
  year = {2012},
  month = {January},
  pages = {25--34},
  isbn = {978-1-4503-1118-2},
  doi = {10.1145/2103746.2103754},
  url = {http://dl.acm.org/citation.cfm?doid=2103746.2103754}
}

ABS is an abstract behavioural specificationA language to model distributed concurrent systems. Characteristic features of ABS are that: (1) it allows abstracting from implementation details while remaining executable: a functional sub-language over abstract data types is used to specify internal, sequential computations; and (2) the imperative sub-language provides flexible concurrency and synchronization mechanisms by means of asynchronous method calls, release points in method definitions, and cooperative scheduling of method activations. This paper presents COSTABS, a COSt and Termination analyzer for ABS, which is able to prove termination and obtain resource usage bounds for both the imperative and functional fragments of programs. The resources that COSTABS can infer include termination, number of execution steps, memory consumption, number of asynchronous calls, among others. The analysis bounds provide formal guarantees that the execution of the program will never exceed the inferred amount of resources. The system can be downloaded as free software from its web site, where a repository of examples and a web interface are also provided. To the best of our knowledge, COSTABS is the first system able to perform resource analysis for a concurrent language.

@inproceedings{AlbertAGGZP12,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Miguel G\'omez-Zamalloa and Germ\'an Puebla},
  title = {{COSTABS}: A {C}ost and {T}ermination {A}nalyzer for {ABS}},
  booktitle = {Proceedings of the 2012 ACM SIGPLAN Workshop on Partial
               Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, 
               January 23-24, 2012},
  publisher = {ACM Press},
  year = {2012},
  month = {January},
  pages = {151-154}
}

One of the main features of programs is the amount of resources which are needed in order to run them. Different resources can be taken into consideration, such as the number of execution steps, amount of memory allocated, number of calls to certain methods, etc. Unfortunately, manually determining the resource consumption of programs is difficult and error-prone. We provide an overview of a state of the art framework for automatically obtaining both upper and lower bounds on the resource consumption of programs. The bounds obtained are functions on the size of the input arguments to the program and are obtained statically, i.e., without running the program. Due to the approximations introduced, the framework can fail to obtain (non-trivial) bounds even if they exist. On the other hand, modulo implementation bugs, the bounds thus obtained are valid for any execution of the program. The framework has been implemented in the COSTA system and can provide useful bounds for realistic object-oriented and actor-based concurrent programs.

@inproceedings{AlbertAGGZP12a,
  author = {Elvira Albert and
               Puri Arenas and
               Samir Genaim and
               Miguel G{\'o}mez-Zamalloa and
               Germ{\'a}n Puebla},
  title = {Automatic {I}nference of {R}esource {C}onsumption {B}ounds},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning
               - 18th International Conference, LPAR-18, M{\'e}rida,
               Venezuela, March 11-15, 2012. ProceedingsLPAR},
  year = {2012},
  pages = {1-11},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7180},
  year = {2012}
}

Cost analysis aims at automatically approximating the resource consumption (e.g., memory) of executing a program in terms of its input parameters. While cost analysis for sequential programming languages has received considerable attention, concurrency and distribution have been notably less studied. The main challenges (and our contributions) of cost analysis in a concurrent setting are: (1) Inferring precise size relations for data in the program in the presence of shared memory. This information is essential for bounding the number of iterations of loops. (2) Distribution suggests that analysis must keep the cost of the diverse distributed components separate. We handle this by means of a novel form of recurrence equations which are parametric on the notion of cost center, which represents a corresponding component. To the best of our knowledge, our work is the first one to present a general cost analysis framework and an implementation for concurrent OO programs.

@inproceedings{AlbertAGGP11,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Miguel G\'{o}mez-Zamalloa and Germ\'an Puebla},
  title = {Cost {A}nalysis of {C}oncurrent {OO} Programs},
  booktitle = {The 9th Asian Symposium on Programming Languages and Systems (APLAS'11)},
  series = {Lecture Notes in Computer Science},
  year = {2011},
  month = {December},
  publisher = {Springer},
  pages = {238-254},
  volume = {7078}
}

@inproceedings{AlbertCPR11,
  author = {Elvira Albert and Jes\'us Correas and Germ\'an Puebla and Guillermo Rom\'an-D\'iez},
  title = {{T}owards {I}ncremental {R}esource {U}sage {A}nalysis},
  booktitle = {The Ninth Asian Symposium on Programming Languages and Systems (APLAS'11)},
  year = {2011},
  month = {December},
  note = {Poster Presentation}
}

Resource guarantees allow being certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. This information can be very useful, especially in real-time and safety-critical applications.Nowadays, a number of automatic tools exist, often based on type systems or static analysis, which produce such resource guarantees. In spite of being based on theoretically sound techniques, the implemented tools may contain bugs which render the resource guarantees thus obtained not completely trustworthy. Performing full-blown verification of such tools is a daunting task, since they are large and complex. In this work we investigate an alternative approach whereby, instead of the tools, we formally verify the results of the tools. We have implemented this idea using COSTA, a state-of-the-art static analysis system, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Our preliminary results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.

@inproceedings{AlbertBGHPR11,
  author = {Elvira Albert and Richard Bubel and Samir Genaim and Reiner H\"ahnle and Germ\'an Puebla and Guillermo Rom\'an-D\'iez},
  title = {{V}erified {R}esource {G}uarantees using {COSTA} and {KeY}},
  booktitle = {Proceedings of the 2011 ACM SIGPLAN Workshop on Partial
               Evaluation and Program Manipulation, PEPM 2011, Austin,
               TX, USA, January 24-25, 2011},
  editor = {Siau-Cheng Khoo and Jeremy G. Siek},
  publisher = {ACM},
  series = {SIGPLAN},
  year = {2011},
  month = {January},
  pages = {73-76}
}

@inproceedings{AlbertGRP10,
  author = {Elvira Albert and Miguel G\'{o}mez-Zamalloa and Jos{\'e} Miguel Rojas and Germ{\'a}n Puebla},
  title = {Compositional {CLP}-based Test Data Generation for Imperative Languages},
  booktitle = {LOPSTR 2010 Revised Selected Papers},
  publisher = {Springer-Verlag},
  series = {LNCS},
  editor = {Mar\'{i}a Alpuente},
  year = {2011},
  volume = {6564},
  pages = {99--116},
  isbn = {978-3-642-20550-7}
}

The paper summarizes a recent work about modular analysis in COSTA.

@inproceedings{RamirezCP10a,
  author = {Diana Ram{\'i}rez-Deantes and Jes{\'u}s Correas and Germ{\'a}n Puebla},
  title = {Modular {T}ermination {A}nalysis of {J}ava {B}ytecode and its {A}pplication to {phoneME} {C}ore {L}ibraries},
  booktitle = {Formal Aspects of Computer Software (FACS 2010)},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = {6921},
  pages = {218--236},
  year = 2011
}

The paper summarizes a recent work about modular analysis in COSTA.

@inproceedings{RamirezCP10,
  author = {Diana Ram{\'i}rez-Deantes and Jes{\'u}s Correas and Germ{\'a}n Puebla},
  title = {Modular {T}ermination {A}nalysis of {J}ava {B}ytecode and its {A}pplication to {phoneME} {C}ore {L}ibraries},
  booktitle = {7th International Workshop on Formal Aspects of Component Software (FACS 2010)},
  butopics = {anal,verif},
  year = {2010},
  month = {October},
  butype = {workshop}
}

Static analysis which takes into account the value of data stored in the heap is typically considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields (or fields for short), i.e., they are field-insensitive. In this paper, we propose locality conditions for soundly converting fields into local variables. This way, field-insensitive analysis over the transformed program can infer information on the original fields. Our notion of locality is context-sensitive and can be applied both to numeric and reference fields. We propose then a polyvariant transformation which actually converts object fields meeting the locality condition into variables and which is able to generate multiple versions of code when this leads to increasing the amount of fields which satisfy the locality conditions. We have implemented our analysis within a termination analyzer for Java bytecode. Interestingly, we can now prove termination of programs which use iterators without the need of a sophisticated heap analysis.

@inproceedings{AlbertAGPR10,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Diana Ram\'{\i}rez-Deantes},
  title = {From Object Fields to Local Variables: A Practical Approach
               to Field-Sensitive Analysis},
  booktitle = {Static Analysis - 17th International Symposium, SAS 2010,
               Perpignan, France, September 14-16, 2010. Proceedings},
  editor = {Radhia Cousot and
               Matthieu Martel},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6337},
  year = {2010},
  month = {September},
  isbn = {978-3-642-15768-4},
  pages = {100-116},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

When describing the resource usage of a program, it is usual to talk in asymptotic terms, such as the well-known “big O” notation, whereby we focus on the behaviour of the program for large input data and make a rough approximation by considering as equivalent programs whose resource usage grows at the same rate. Motivated by the existence of non-asymptotic resource usage analyzers, in this paper, we develop a novel transformation from a non-asymptotic cost function (which can be produced by multiple resource analyzers) into its asymptotic form. Our transformation aims at producing tight asymptotic forms which do not contain redundant subexpressions (i.e., expressions asymptotically subsumed by others). Interestingly, we integrate our transformation at the heart of a cost analyzer to generate asymptotic upper bounds without having to first compute their non-asymptotic counterparts. Our experimental results show that, while non-asymptotic cost functions become very complex, their asymptotic forms are much more compact and manageable. This is essential to improve scalability and to enable the application of cost analysis in resource-aware verification/certification.

@inproceedings{AlbertAAGP09,
  author = {Elvira Albert and Diego Alonso and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla},
  title = {Asymptotic {R}esource {U}sage {B}ounds},
  booktitle = {The Seventh Asian Symposium on Programming Languages and Systems (APLAS'09)},
  year = 2009,
  month = {December},
  editor = {Zhenjiang Hu},
  series = {Lecture Notes in Computer Science},
  volume = {5904},
  pages = {294-310},
  publisher = {Springer},
  slides = {http://costa.ls.fi.upm.es/papers/costa/AlbertAAGP09-slides.pdf}
}

COSTA is a static analyzer for Java bytecode which is able to infer cost and termination information for large classes of programs. The analyzer takes as input a program and a resource of interest, in the form of a cost model, and aims at obtaining an upper bound on the execution cost with respect to the resource and at proving program termination. The COSTA system has reached a considerable degree of maturity in that (1) it includes state-of-the-art techniques for statically estimating the resource consumption and the termination behavior of programs, plus a number of specialized techniques which are required for achieving accurate results in the context of object-oriented programs, such as handling numeric fields in value analysis; (2) it provides several non-trivial notions of cost (resource consumption) including, in addition to the number of execution steps, the amount of memory allocated in the heap or the number of calls to some user-specified method; (3) it provides several user interfaces: a classical command line, a Web interface which allows experimenting remotely with the system without the need of installing it locally, and a recently developed Eclipse plugin which facilitates usage of the analyzer, even during the development phase; (4) it can deal with both the Standard and Micro editions of Java. In the tool demonstration, we will show that COSTA is able to produce meaningful results for non-trivial programs, possibly using Java libraries. Such results can then be used in many applications, including program development, resource usage certification, program optimization, etc.

@inproceedings{AlbertAGGPRRZ09,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Miguel G{\'o}mez-Zamalloa and Germ{\'a}n Puebla and Diana Ramirez and Guillermo Rom\'an-D\'iez and Damiano Zanardini},
  title = {{T}ermination and {C}ost {A}nalysis with {COSTA} and its {U}ser {I}nterfaces},
  booktitle = {Spanish Conference on Programming and Computer Languages (PROLE'09)},
  series = {ENTCS},
  publisher = {Elsevier},
  volume = {258},
  year = {2009},
  pages = {109-121},
  month = {September}
}

@inproceedings{AlbertGP08,
  author = {Elvira Albert and Miguel G\'{o}mez-Zamalloa and Germ{\'a}n Puebla},
  title = {{T}est {D}ata {G}eneration of {B}ytecode by {CLP} {P}artial {E}valuation},
  booktitle = {18th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'08)},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {5438},
  pages = {4--23},
  month = {March},
  year = {2009}
}

Shared mutable data structures pose major problems in static analysis and most analyzers are unable to keep track of the values of numeric variables stored in the heap. In this paper, we first identify sufficient conditions under which heap allocated numeric variables in object oriented programs (i.e., numeric fields) can be handled as non-heap allocated variables. Then, we present a static analysis to infer which numeric fields satisfy these conditions at the level of (sequential) bytecode. This allows instrumenting the code with ghost variables which make such numeric fields observable to any field-insensitive value analysis. Our experimental results in termination analysis show that we greatly enlarge the class of analyzable programs with a reasonable overhead.

@inproceedings{AlbertAGP09,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla},
  title = {{F}ield-{S}ensitive {V}alue {A}nalysis by {F}ield-{I}nsensitive {A}nalysis},
  booktitle = {16th International Symposium on Formal Methods, FM'09},
  year = 2009,
  editor = {Ana Cavalcanti and Dennis Dams},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = {5850},
  pages = {370-386},
  isbn = {978-3-642-05088-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Cost analysis aims at obtaining information about the execution cost of programs. This paper studies cost relation systems (CESs): the sets of recursive equations used in cost analysis in order to capture the execution cost of programs in terms of the size of their input arguments. We investigate the notion of CES from a general perspective which is independent of the particular cost analysis framework. Our main contributions are: we provide a formal definition of execution cost and of CES which is not tied to a particular programming language; we present the notion of sound CES, i.e., which correctly approximates the cost of the corresponding program; we identify the differences with recurrence relation systems, its possible applications and the new challenges that they bring about. Our general framework is illustrated by instantiating it to cost analysis of Java bytecode, Haskell, and Prolog.

@inproceedings{AlbertAGP08b,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla},
  title = {{C}ost {R}elation {S}ystems: a
               {L}anguage--{I}ndependent {T}arget {L}anguage for
               {C}ost {A}nalysis},
  booktitle = {Spanish Conference on Programming and Computer Languages (PROLE'08)},
  series = {ENTCS},
  volume = {248},
  year = {2009},
  pages = {31-46},
  publisher = {Elsevier},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Gomez-ZAP08,
  author = {Miguel G\'{o}mez-Zamalloa and Elvira Albert and Germ{\'a}n Puebla},
  title = {{M}odular {D}ecompilation of {L}ow-{L}evel {C}ode by {P}artial {E}valuation},
  booktitle = {8th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM'08)},
  publisher = {IEEE Computer Society},
  year = {2008},
  pages = {239--248},
  month = {September}
}

This paper describes COSTA, a cost and termination analyzer for Java bytecode. The system receives as input a bytecode program and a selection of a resources of interest, and tries to bound the resource consumption of the program with respect to such a cost model. COSTA provides several non-trivial notions of resource, as the consumption of the heap, the number of bytecode instructions executed, the number of calls to a specific method (e.g., the library method for sending text messages in mobile phones), etc. The system uses the same machinery to infer upper bounds on cost, and for proving termination (which also implies the boundedness of any resource consumption). The demo will describe the architecture of COSTA and show it on a series of programs for which interesting bounds w.r.t. the above notions of resource can be obtained. Also, examples for which the system cannot obtain upper bounds, but can prove termination, will be presented.

@inproceedings{AlbertAGPZ08a,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Damiano Zanardini},
  title = {{COSTA}: {A} {C}ost and {T}ermination {A}nalyzer for {J}ava {B}ytecode},
  booktitle = {Proceedings of the Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode)},
  year = 2008,
  series = {Electronic Notes in Theoretical Computer Science},
  address = {Budapest, Hungary},
  month = {April},
  publisher = {Elsevier},
  note = {To appear in ENTCS}
}

@inproceedings{AlbertGGP08,
  author = {Elvira Albert and John P. Gallagher and Miguel G\'{o}mez-Zamalloa and Germ{\'a}n Puebla},
  title = {{T}ype-based {H}omeomorphic {E}mbedding and its
                  {A}pplications to {O}nline {P}artial {E}valuation},
  booktitle = {17th International Symposium on Logic-based Program
                  Synthesis and Transformation (LOPSTR'07)},
  publisher = {Springer-Verlag},
  series = {LNCS},
  volume = {4915},
  pages = {23--42},
  npages = 20,
  year = {2008},
  month = {February}
}

@inproceedings{AlbertAGPZ08c,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ\'an Puebla and D.~Zanardini},
  title = {{\sc COSTA}: {D}esign and {I}mplementation of a {C}ost and
 {T}ermination {A}nalyzer for {J}ava {B}ytecode},
  booktitle = {6th International Symposium on Formal Methods for Components and Objects (FMCO'07)},
  year = 2008,
  month = {February},
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {anal},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  number = {5382},
  pages = {113-133}
}

COSTA is a research prototype which performs automatic program analysis and which is able to infer cost and termination information about Java bytecode programs. The system receives as input a bytecode program and a cost model chosen from a selection of resource descriptions, and tries to bound the resource consumption of the program with respect to the given cost model. COSTA provides several non-trivial notions of resource, such as the amount of memory allocated on the heap, the number of bytecode instructions executed, the number of billable events (such as sending a text message on a mobile phone) executed by the program. When performing cost analysis, COSTA produces a cost equation system, which is an extended form of recurrence relations. In order to obtain a closed (i.e., non-recursive) form for such recurrence relations which represents an upper bound, COSTA includes a dedicated solver. An interesting feature of COSTA is that it uses pretty much the same machinery for inferring upper bounds on cost as for proving termination (which also implies the boundedness of any resource consumption).

@inproceedings{AlbertAGP08,
  author = {Elvira Albert and
               Puri Arenas and
               Samir Genaim and
               Germ{\'a}n Puebla},
  title = {Automatic Inference of Upper Bounds for Recurrence Relations
               in Cost Analysis},
  booktitle = {Static Analysis, 15th International Symposium, SAS 2008,
               Valencia, Spain, July 16-18, 2008. Proceedings},
  editor = {Mar\'{\i}a Alpuente and
               Germ{\'a}n Vidal},
  year = {2008},
  pages = {221-237},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5079},
  isbn = {978-3-540-69163-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Termination analysis has received considerable attention, traditionally in the context of declarative programming, and recently also for imperative languages. In existing approaches, termination is performed on source programs. However, there are many situations, including mobile code, where only the compiled code is available. In this work we present an automatic termination analysis for sequential Java Bytecode programs. Such analysis presents all of the challenges of analyzing a low-level language as well as those introduced by object-oriented languages. Interestingly, given a bytecode program, we produce a constraint logic program, CLP, whose termination entails termination of the bytecode program. This allows applying the large body of work in termination of CLP programs to termination of Java bytecode. A prototype analyzer is described and initial experimentation is reported.

@inproceedings{AlbertACGPZ08,
  author = {Elvira Albert and
               Puri Arenas and
               Michael Codish and
               Samir Genaim and
               Germ{\'a}n Puebla and
               Damiano Zanardini},
  title = {Termination Analysis of Java Bytecode},
  booktitle = {Formal Methods for Open Object-Based Distributed Systems,
               10th IFIP WG 6.1 International Conference, FMOODS 2008,
               Oslo, Norway, June 4-6, 2008, Proceedings},
  editor = {Gilles Barthe and Frank S. de Boer},
  year = {2008},
  pages = {2-18},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5051},
  isbn = {978-3-540-68862-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Automatic cost analysis has interesting applications in the context of verification and certification of mobile code. For instance, the code receiver can use cost information in order to decide whether to reject mobile code which has too large cost requirements in terms of computing resources (in time and/or space) or billable events (SMSs sent, bandwidth required). Existing cost analyses for a variety of languages describe the resource consumption of programs by means of Cost Equation Systems (CESs), which are similar to, but more general than recurrence equations. CESs express the cost of a program in terms of the size of its input data. In a further step, a closed form (i.e., non-recursive) solution or upper bound can sometimes be found by using existing Computer Algebra Systems (CASs), such as Maple and Mathematica. In this work, we focus on cost analysis of Java bytecode, a language which is widely used in the context of mobile code and we study the problem of identifying variables which are useless in the sense that they do not affect the execution cost and therefore can be ignored by cost analysis. We identify two classes of useless variables and propose automatic analysis techniques to detect them. The first class corresponds to stack variables that can be replaced by program variables or constant values. The second class corresponds to variables whose value is cost-irrelevant, i.e., does not affect the cost of the program. We propose an algorithm, inspired in static slicing which safely identifies cost-irrelevant variables. The benefits of eliminating useless variables are two-fold: (1) cost analysis without useless variables can be more efficient and (2) resulting CESs are more likely to be solvable by existing CASs.

@inproceedings{AlbertAGPZ08,
  author = {Elvira Albert and
               Puri Arenas and
               Samir Genaim and
               Germ{\'a}n Puebla and
               Damiano Zanardini},
  title = {Removing useless variables in cost analysis of Java bytecode},
  editor = {Roger L. Wainwright and
               Hisham Haddad},
  booktitle = {Proceedings of the 2008 ACM Symposium on Applied Computing
               (SAC), Fortaleza, Ceara, Brazil, March 16-20, 2008},
  year = {2008},
  pages = {368-375},
  publisher = {ACM},
  isbn = {978-1-59593-753-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

This paper describes the architecture of COSTA, an abstract interpretation based cost and termination analyzer for Java bytecode. The system receives as input a bytecode program, (a choice of) a resource of interest and tries to obtain an upper bound of the resource consumption of the program. COSTA provides several non-trivial notions of cost, as the consumption of the heap, the number of bytecode instructions executed and the number of calls to a specific method. Additionally, COSTA tries to prove termination of the bytecode program which implies the boundedness of any resource consumption. Having cost and termination together is interesting, as both analyses share most of the machinery to, respectively, infer cost upper bounds and to prove that the execution length is always finite (i.e., the program terminates). We report on experimental results which show that COSTA can deal with programs of realistic size and complexity, including programs which use Java libraries. To the best of our knowledge, this system provides for the first time evidence that resource usage analysis can be applied to a realistic object-oriented, bytecode programming language.

@inproceedings{AlbertAGPZ07d,
  author = {Elvira Albert and
               Puri Arenas and
               Samir Genaim and
               Germ{\'a}n Puebla and
               Damiano Zanardini},
  title = {{COSTA}: Design and Implementation of a Cost and Termination
               Analyzer for Java Bytecode},
  booktitle = {Formal Methods for Components and Objects, 6th International
               Symposium, FMCO 2007, Amsterdam, The Netherlands, October
               24-26, 2007, Revised Lectures},
  pages = {113-132},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5382},
  year = {2008},
  isbn = {978-3-540-92187-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{mod-types-pepm08,
  author = {P.~Pietrzak and Jes\'us Correas and Germ\'an Puebla and
                  M.~Hermenegildo},
  title = {{A} {P}ractical {T}ype {A}nalysis for {V}erification of
                  {M}odular {P}rolog {P}rograms},
  booktitle = {ACM SIGPLAN 2008 Workshop on Partial Evaluation and
                  Program Manipulation (PEPM'08)},
  year = 2008,
  month = {January},
  pages = {61--70},
  publisher = {{ACM} {P}ress},
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {anal,debug},
  paper_presentation_city = {San Francisco},
  paper_presentation_country = {US},
  buconfj = {pepm},
  isbn = {ISBN 978-1-59593-977-7}
}

Cost analysis of Java bytecode is complicated by its unstructured control flow, the use of an operand stack and its object-oriented programming features (like dynamic dispatching). This paper addresses these problems and develops a generic framework for the automatic cost analysis of sequential Java bytecode. Our method generates cost relations which define at compile-time the cost of programs as a function of their input data size. To the best of our knowledge, this is the first approach to the automatic cost analysis of Java bytecode.

@inproceedings{AlbertAGPZ07b,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Damiano Zanardini},
  title = {A {G}eneric {F}ramework for the {C}ost {A}nalysis of {J}ava {B}ytecode},
  booktitle = {Spanish Conference on Programming and Computer Languages (PROLE'07)},
  year = {2007},
  pages = {61-70},
  month = {September},
  editor = {Pimentel Ernesto}
}

Recently, we proposed a general framework for the cost analysis of Java bytecode which can be used for measuring resource usage. This analysis generates, at compile-time, cost relations which define the cost of programs as a function of their input data size. The purpose of this paper is to assess the practicality of such cost analysis by experimentally evaluating a prototype analyzer implemented in CIAO. With this aim, we approximate the computational complexity of a set of selected benchmarks, including both well-known algorithms which have been used to evaluate existing cost analyzers in other programming paradigms, and other benchmarks which illustrate object-oriented features. In our evaluation, we first study whether the generated cost relations can be automatically solved. Our experiments show that in some cases the inferred cost relations can be automatically solved by using the Mathmatica system, whereas, in other cases, some prior manipulation is required for the equations to be solvable. Moreover, we experimentally evaluated the running time of the different phases of the analysis process. Overall, we believe our experiments show that the efficiency of our cost analysis is acceptable, and that the obtained cost relations are useful in practice since, at least in our experiments, it is possible to get a closed form solution.

@inproceedings{AlbertAGPZ07a,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Damiano Zanardini},
  title = {{E}xperiments in {C}ost {A}nalysis of {J}ava {B}ytecode},
  booktitle = {2nd Workshop on Bytecode Semantics, Verification, Analysis and Transformations, BYTECODE 2007, April 1, 2007, Braga, Portugal},
  pages = {67-83},
  year = 2007,
  editor = {Fausto Spoto and Marieke Huisman},
  volume = {190},
  series = {Electronic Notes in Theoretical Computer Science},
  month = {April},
  publisher = {Elsevier}
}

Cost analysis of Java bytecode is complicated by its unstructured control flow, the use of an operand stack and its object-oriented programming features (like dynamic dispatching). This paper addresses these problems and develops a generic framework for the automatic cost analysis of sequential Java bytecode. Our method generates cost relations which define at compile-time the cost of programs as a function of their input data size. To the best of our knowledge, this is the first approach to the automatic cost analysis of Java bytecode.

@inproceedings{AlbertAGPZ07,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Damiano Zanardini},
  title = {{C}ost {A}nalysis of {J}ava {B}ytecode},
  booktitle = {16th European Symposium on Programming, ESOP'07},
  year = 2007,
  editor = {Rocco De Nicola},
  series = {Lecture Notes in Computer Science},
  month = {March},
  publisher = {Springer-Verlag},
  volume = {4421},
  pages = {157-172},
  isbn = {978-3-540-71314-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{AlbertGHP07,
  author = {Elvira Albert and Miguel G\'{o}mez-Zamalloa and Laurent Hubert and Germ{\'a}n Puebla},
  title = {{V}erification of {J}ava {B}ytecode using {A}nalysis and
                  {T}ransformation of {L}ogic {P}rograms},
  booktitle = {Ninth International Symposium on Practical Aspects of
                  Declarative Languages (PADL 2007)},
  year = 2007,
  month = {January},
  pages = {124--139},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {4354}
}

@inproceedings{estim-exec-time-padl07,
  author = {E.~Mera and P. L\'{o}pez-Garc\'{\i}a and Germ\'an Puebla and
                  M.~Carro and M. Hermenegildo},
  title = {{C}ombining {S}tatic {A}nalysis and {P}rofiling for
                  {E}stimating {E}xecution {T}imes},
  booktitle = {Ninth International Symposium on Practical Aspects of
                  Declarative Languages (PADL'07)},
  pages = {140--154},
  year = 2007,
  month = {January},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {4354},
  buconfj = {padl},
  projects = {MOBIUS,MERIT,PROMESAS,POAIST},
  paper_presentation_city = {Nice},
  paper_presentation_country = {France},
  butopics = {anal,gran}
}

@inproceedings{pcpe-pepm07,
  author = {C.~Ochoa and Germ\'an Puebla},
  title = {{P}oly-{C}ontrolled {P}artial {E}valuation in {P}ractice},
  booktitle = {ACM Partial Evaluation and Program Manipulation
                  (PEPM'07)},
  year = 2007,
  month = {January},
  pages = {164--173},
  paper_presentation_city = {Nice},
  paper_presentation_country = {France},
  publisher = {{ACM} {P}ress},
  butopics = {spec,anal},
  buconfj = {pepm},
  projects = {MOBIUS,MERIT,PROMESAS},
  isbn = {ISBN 978-1-59593-620-2}
}

@inproceedings{inc-acc-lpar06,
  author = {Elvira Albert and Puri Arenas and Germ\'an Puebla},
  title = {An {I}ncremental {A}pproach to
{A}bstraction-{C}arrying {C}ode},
  booktitle = { 13th International Conference on
Logic for Programming, Artificial Intelligence, and
Reasoning (LPAR'06)},
  year = 2006,
  month = {November},
  npages = 15,
  pages = {377--391},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {4246},
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {anal,debug},
  buconfj = {lpar},
  paper_presentation_city = {Phnom Penh},
  paper_presentation_country = {Cambodia}
}

@inproceedings{mod-ctchecks-lpar06,
  author = {P.~Pietrzak and Jes\'us Correas and Germ\'an Puebla and
                  M.~Hermenegildo},
  title = {{C}ontext-{S}ensitive {M}ultivariant {A}ssertion {C}hecking
                  in {M}odular {P}rograms},
  booktitle = {13th International Conference on Logic for Programming
                  Artificial Intelligence and Reasoning (LPAR'06)},
  year = 2006,
  month = {November},
  npages = 15,
  pages = {392--406},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {4246},
  projects = {MOBIUS,MERIT,PROMESAS,POAIST},
  butopics = {anal,debug},
  paper_presentation_city = {Phnom Penh},
  paper_presentation_country = {Cambodia},
  buconfj = {lpar}
}

@inproceedings{carro06:stream_interpreter_cases,
  author = {M.~Carro and J.~Morales and H.L.~Muller and Germ\'an Puebla and
                  M.~Hermenegildo},
  title = {{H}igh-{L}evel {L}anguages for {S}mall {D}evices: {A}
                  {C}ase {S}tudy},
  booktitle = {Compilers, Architecture, and Synthesis for Embedded
                  Systems},
  npages = 11,
  year = 2006,
  pages = {271-281},
  editor = {Krisztian Flautner and Taewhan Kim},
  month = {October},
  publisher = {ACM Press / Sheridan},
  buconfj = {cases},
  butopics = {impl,spec,lang},
  paper_presentation_city = {Seoul},
  paper_presentation_country = {Korea},
  projects = {ASAP,POAIST,MERIT,PROMESAS}
}

@inproceedings{estim-exec-time-poster,
  author = {E.~Mera and P. L\'{o}pez-Garc\'{\i}a and Germ\'an Puebla and
                  M.~Carro and M. Hermenegildo},
  title = {{U}sing {C}ombined {S}tatic {A}nalysis and {P}rofiling
            for {L}ogic {P}rogram {E}xecution {T}ime {E}stimation},
  booktitle = {22nd International Conference on Logic Programming
                  (ICLP'06)},
  pages = {431--432},
  year = 2006,
  month = {August},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {4079},
  projects = {MOBIUS,MERIT,PROMESAS,POAIST},
  butopics = {anal,gran},
  paper_presentation_city = {Seattle, Washington},
  paper_presentation_country = {USA},
  buconfj = {iclp}
}

@inproceedings{ai-with-specs-sas06,
  author = {Germ\'an Puebla and Elvira Albert and M.~Hermenegildo},
  title = {{A}bstract {I}nterpretation with {S}pecialized
                  {D}efinitions},
  booktitle = {The 13th International Static Analysis Symposium
                  (SAS'06)},
  year = 2006,
  month = {August},
  publisher = {Springer},
  series = {LNCS},
  number = {4134},
  pages = {107--126},
  paper_presentation_city = {Seoul},
  paper_presentation_country = {Korea},
  butopics = {anal,spec},
  projects = {MOBIUS, MERIT, POAIST,PROMESAS},
  buconfj = {sas}
}

@inproceedings{ai-safety-reduced-iclp06,
  author = {Elvira Albert and Puri Arenas and Germ\'an Puebla and M. Hermenegildo},
  title = {{R}educed {C}ertificates for {A}bstraction-{C}arrying
                  {C}ode},
  booktitle = {22nd International Conference on Logic Programming (ICLP
                  2006)},
  year = {2006},
  month = {August},
  pages = {163--178},
  paper_presentation_city = {Seattle, Washington},
  paper_presentation_country = {USA},
  projects = {MERIT,MOBIUS,POAIST,PROMESAS},
  butopics = {anal,debug},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {4079},
  buconfj = {iclp}
}

@inproceedings{minunf-lopstr05,
  author = {C.~Ochoa and Germ\'an Puebla and M.~Hermenegildo},
  title = {{R}emoving {S}uperfluous {V}ersions in {P}olyvariant
                  {S}pecialization of {P}rolog {P}rograms},
  booktitle = {15th International Symposium on Logic-based Program
                  Synthesis and Transformation (LOPSTR'05)},
  year = {2006},
  month = {April},
  pages = {80--97},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {3901},
  paper_presentation_city = {London},
  paper_presentation_country = {United Kingdom},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {spec,anal},
  buconfj = {lopstr}
}

@inproceedings{nonleftmost-lopstr05,
  author = {Elvira Albert and Germ\'an Puebla and J.~Gallagher},
  title = {{N}on-{L}eftmost {U}nfolding in {P}artial {E}valuation of
                 {L}ogic {P}rograms with {I}mpure {P}redicates},
  booktitle = {15th International Symposium on Logic-based Program
                  Synthesis and Transformation (LOPSTR'05)},
  year = {2006},
  month = {April},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {3901},
  pages = {115--132},
  paper_presentation_city = {London},
  paper_presentation_country = {United Kingdom},
  projects = {ASAP,CUBICO,MOBIUS},
  butopics = {spec,anal},
  buconfj = {lopstr}
}

@inproceedings{type-domains-lopstr05,
  author = {J.~Gallagher and Germ\'an Puebla and Elvira Albert },
  title = {Converting one {T}ype-{B}ased {A}bstract {D}omain to
                  {A}nother},
  booktitle = {15th International Symposium on Logic-based Program
                  Synthesis and Transformation (LOPSTR'05)},
  year = {2006},
  month = {April},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {3901},
  pages = {147--162},
  paper_presentation_city = {London},
  paper_presentation_country = {United Kingdom},
  projects = {ASAP,CUBICO,MOBIUS},
  butopics = {anal},
  buconfj = {lopstr}
}

@inproceedings{modbenchmarks-lopstr05,
  author = {Jes\'us Correas and Germ\'an Puebla and M.~Hermenegildo and
                  F.~Bueno},
  title = {{E}xperiments in {C}ontext-{S}ensitive {A}nalysis of
                  {M}odular {P}rograms},
  booktitle = {15th International Symposium on Logic-based Program
                  Synthesis and Transformation (LOPSTR'05)},
  year = {2006},
  month = {April},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {3901},
  pages = {163--178},
  paper_presentation_city = {London},
  paper_presentation_country = {United Kingdom},
  projects = {ASAP,CUBICO,POAIST,MOBIUS},
  butopics = {anal},
  buconfj = {lopstr}
}

@inproceedings{pcpd-ppdp06,
  author = {Germ\'an Puebla and C.~Ochoa},
  title = {{P}oly-{C}ontrolled {P}artial {E}valuation},
  booktitle = {8th ACM{-}SIGPLAN International Symposium on
                  Principles and Practice of Declarative Programming
                  (PPDP'06)},
  year = {2006},
  publisher = {ACM Press},
  paper_presentation_city = {Venice},
  paper_presentation_country = {Italy},
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {spec,anal},
  buconfj = {ppdp}
}

@inproceedings{morales05:generic_eff_AM_implem_iclp,
  author = {J. Morales and M.~Carro and Germ\'an Puebla and
                  M. Hermenegildo},
  title = {{A Generator of Efficient Abstract Machine Implementations
      and its Application to Emulator Minimization}},
  booktitle = {International Conference on Logic Programming},
  pages = {21--36},
  year = 2005,
  editor = {Maurizio Gabbrielli and Gopal Gupta},
  series = {LNCS},
  number = {3668},
  month = {October},
  publisher = {Springer Verlag},
  buconfj = {iclp},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {impl}
}

@inproceedings{ai-spec-defs-poster,
  author = {Germ\'an Puebla and Elvira Albert and M.~Hermenegildo},
  title = {A {G}eneric {F}ramework for the {A}nalysis and
                 {S}pecialization of Logic Programs},
  booktitle = {International Conference on Logic Programming (ICLP
                  2005)},
  year = 2005,
  month = {October},
  series = {LNCS},
  editor = {Maurizio Gabbrielli and Gopal Gupta},
  number = {3668},
  pages = {407-409},
  publisher = {Springer},
  note = {Extended Abstract},
  butopics = {anal,spec},
  projects = {ASAP,CUBICO,POAIST},
  buconfj = {iclp}
}

@inproceedings{lopstr04-unfolding,
  author = {Germ\'an Puebla and Elvira Albert and M.~Hermenegildo},
  title = {Efficient {L}ocal {U}nfolding with {A}ncestor {S}tacks for
                  {F}ull {P}rolog},
  booktitle = {14th International Symposium on Logic-based Program
                  Synthesis and Transformation (LOPSTR'04)},
  year = {2005},
  month = {August},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {3573},
  pages = {149--165},
  paper_presentation_city = {Verona},
  paper_presentation_country = {Italy},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {spec},
  buconfj = {lopstr}
}

@inproceedings{lpar04-ai-safety-long,
  author = {Elvira Albert and Germ\'an Puebla and M.~Hermenegildo},
  title = {{A}bstraction-{Carrying} {Code} },
  booktitle = {11th International Conference on Logic for Programming
Artificial Intelligence and Reasoning (LPAR 2004)},
  publisher = {Springer-Verlag},
  series = {LNAI},
  number = {3452},
  year = {2005},
  npages = 17,
  month = {March},
  paper_presentation_city = {Montevideo},
  paper_presentation_country = {Uruguay},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {anal,debug},
  buconfj = {lpar},
  pages = {380--397},
  issn = {ISSN 0302-9743}
}

@inproceedings{smc04-ai-safety,
  author = {Elvira Albert and Germ\'an Puebla and M.~Hermenegildo},
  title = {Experiments in {A}bstract {I}nterpretation-based {C}ode
  {C}ertification for {P}ervasive {S}ystems},
  booktitle = {Proc. of 2004 IEEE Conference on Systems, Man \&
                  Cybernetics
(Special Session on Correctness and Reliability for
                  Pervasive/Ubiquitous Computing)},
  year = {2004},
  month = {October},
  publisher = {IEEE},
  isbn = {ISBN 0-7803-8567-5},
  npages = 6,
  paper_presentation_city = {The Hague},
  paper_presentation_country = {Netherlands},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {anal,debug},
  buconfj = {smc}
}

@inproceedings{iclp04-ai-safety,
  author = {Elvira Albert and Germ\'an Puebla and M.~Hermenegildo},
  title = {{A}bstract {I}nterpretation-based {M}obile {C}ode
  {C}ertification},
  booktitle = {Proc. of International Conference on Logic Programming
                  (ICLP'04)},
  year = {2004},
  month = {September},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {3132},
  pages = {446-447},
  paper_presentation_city = {Saint-Malo},
  paper_presentation_country = {France},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {anal,debug},
  buconfj = {iclp},
  note = {Extended Abstract},
  isbn = {ISBN 3-540-22671-0},
  issn = {ISSN 0302-9743}
}

@inproceedings{set-based-absint-padl,
  author = {J.~Gallagher and Germ\'an Puebla},
  title = {{A}bstract {I}nterpretation over {N}on-{D}eterministic
                  {F}inite {T}ree {A}utomata for {S}et-{B}ased
                  {A}nalysis of {L}ogic {P}rograms},
  booktitle = {Fourth International Symposium on
               Practical Aspects of Declarative Languages},
  year = 2002,
  series = {LNCS},
  number = {2257},
  month = {January},
  publisher = {Springer-Verlag},
  pages = {243--261},
  butopics = {anal,debug},
  buconfj = {padl},
  projects = {EDIPIA, ADELA}
}

@inproceedings{assrt-theoret-framework-lopstr99,
  author = {Germ\'an Puebla and F.~Bueno and M.~Hermenegildo},
  title = {{C}ombined {S}tatic and {D}ynamic {A}ssertion-{B}ased
                  {D}ebugging of {C}onstraint {L}ogic {P}rograms},
  booktitle = {Logic-based Program Synthesis and Transformation
                  (LOPSTR'99)},
  year = 2000,
  series = {LNCS},
  month = {March},
  number = {1817},
  publisher = {Springer-Verlag},
  pages = {273--292},
  buconfj = {lopstr},
  butopics = {debug,anal},
  projects = {DISCIPL,EDIPIA}
}

@inproceedings{assrt-framework-cp98,
  author = {Germ\'an Puebla and F.~Bueno and M.~Hermenegildo},
  title = {{A} {F}ramework for {A}ssertion-based {D}ebugging in
                  {C}onstraint {L}ogic {P}rogramming (abstract)},
  booktitle = {Proceedings of the International Conference on
                  Principles and Practice of Constraint Programming
                  (CP'98)},
  year = {1998},
  month = {October},
  pages = {472--473},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  series = {LNCS},
  number = {1520},
  editors = {M.~Maher and J.-F.~Puget},
  address = {Pisa, Italy},
  butopics = {debug,anal},
  buconfj = {cp},
  projects = {ELLA, DISCIPL}
}

@inproceedings{tools-env-abstract,
  author = {Germ\'an Puebla and M.~Comini and W.~Drabent and M.~Ducass and
                  M.~Fabris and M.~Meier and Ch.~Schulte},
  title = {{T}ools and {E}nvironments for {C}onstraint {L}ogic
                  {P}rogramming},
  booktitle = {International Logic Programming Symposium},
  year = 1997,
  month = {October},
  pages = {417--418},
  note = {Workshop abstract},
  butopics = {debug,misc}
}

@inproceedings{spec-dyn-sch-iclp97,
  author = {Germ\'an Puebla and M.~{Garc\'{\i}a de la Banda} and K.~Marriott
                  and P.~Stuckey},
  title = {{O}ptimization of {L}ogic {P}rograms with {D}ynamic
                  {S}cheduling},
  booktitle = {1997 International Conference on Logic Programming},
  pages = {93--107},
  year = {1997},
  month = {June},
  publisher = {MIT Press},
  address = {Cambridge, MA},
  publisher_location = {Cambridge, MA, USA},
  butopics = {conc,anal,spec},
  buconfj = {iclp},
  paper_presentation_city = {Leuven},
  paper_presentation_country = {Belgium}
}

@inproceedings{inc-fixp-sas,
  author = {Germ\'an Puebla and M.~Hermenegildo},
  title = {{O}ptimized {A}lgorithms for the {I}ncremental {A}nalysis
                  of {L}ogic {P}rograms},
  booktitle = {International Static Analysis Symposium (SAS 1996)},
  pages = {270--284},
  year = {1996},
  month = {September},
  publisher = {Springer-Verlag},
  number = 1145,
  series = {{LNCS}},
  publisher_location = {Heidelberg, Germany},
  paper_presentation_city = {Aachen},
  paper_presentation_country = {Germany},
  butopics = {anal},
  buconfj = {sas}
}

@inproceedings{inc-fixp-sas-semi-short,
  author = {Germ\'an Puebla and M.~Hermenegildo},
  title = {{O}ptimized {A}lgorithms for the {I}ncremental {A}nalysis
                  of {L}ogic {P}rograms},
  booktitle = {International Static Analysis Symposium (SAS 1996)},
  pages = {270--284},
  year = {1996},
  publisher = {Springer-Verlag},
  number = 1145,
  series = {{LNCS}},
  butopics = {anal},
  buconfj = {sas}
}

@inproceedings{spec-pepm,
  author = {Germ\'an Puebla and M.~Hermenegildo},
  title = {{I}mplementation of {M}ultiple {S}pecialization in {L}ogic
                  {P}rograms},
  booktitle = {Proc. {ACM} {SIGPLAN} Symposium on Partial Evaluation
                  and Semantics Based Program Manipulation},
  pages = {77--87},
  year = {1995},
  month = {June},
  publisher = {{ACM} {P}ress},
  butopics = {spec,anal},
  buconfj = {pepm},
  projects = {PARFORCE, IPL-D},
  paper_presentation_city = {La Jolla, California},
  paper_presentation_country = {USA}
}

In this tutorial paper, we overview the techniques that un- derlie the automatic inference of resource consumption bounds. We first explain the basic techniques on a Java-like sequential language. Then, we describe the extensions that are required to apply our method on concurrent ABS programs. Finally, we discuss some advanced issues in resource analysis, including the inference of non-cumulative resources and the treatment of shared mutable data.

@article{FmcoTutorial12,
  title = {{A}utomatic {I}nference of {B}ounds on {R}esource {C}onsumption},
  author = {Elvira Albert and Diego Alonso-Blas and Puri Arenas and Jes\'us Correas and Antonio Flores-Montoya and Samir Genaim and Miguel G\'omez-Zamalloa and Abu Naser Masud and Germ\'an Puebla and Jos\'e Miguel Rojas and Guillermo Rom\'an-D\'iez and Damiano Zanardini},
  booktitle = {HATS International School on Formal Models for Objects and Components 2012. Tutorial Lectures},
  year = 2013,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  note = {To Appear in Lecture Notes in Computer Science}
}

Resource usage is one of the most important characteristics of programs. Automatically generated information about resource usage can be used in multiple ways, both during program development and deployment. In this paper we discuss and present examples on how such information is obtained in COSTA, a state of the art static analysis system. COSTA obtains safe symbolic upper bounds on the resource usage of a large class of general-purpose programs written in a mainstream programming language such as Java (bytecode). We also discuss the application of resource-usage information for code certification, whereby code not guaranteed to run within certain user-specified bounds is rejected.

@incollection{AlbertAGPZ09,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Damiano Zanardini},
  title = {Resource Usage Analysis and its Application to Resource Certification},
  booktitle = {Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures},
  editor = {Alessandro Aldini and Gilles Barthe and Roberto Gorrieri},
  pages = {258-288},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5705},
  year = {2009},
  isbn = {978-3-642-03828-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection{hermenegildo08:ciao-design-ugo-fest,
  author = {M. V. Hermenegildo and F. Bueno and M. Carro and 
                  P. L\'{o}pez and J.F. Morales and Germ\'an Puebla},
  title = {{A}n {O}verview of {T}he {C}iao {M}ultiparadigm {L}anguage
                  and {P}rogram {D}evelopment {E}nvironment
                  and its {D}esign {P}hilosophy},
  booktitle = {{F}estschrift for {U}go {M}ontanari},
  editor = {Pierpaolo Degano and Rocco De Nicola and Jose Meseguer},
  year = 2008,
  month = {June},
  pages = {209--237},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  series = {LNCS},
  number = {5065},
  butopics = {lang,impl,autop,debug,env,anal,spec,gran},
  projects = {MOBIUS,MERIT,PROMESAS,SCUBE,POAIST}
}

@incollection{mod-an-lopstrbook,
  author = {Germ\'an Puebla and Jes\'us Correas and M.~Hermenegildo and F.~Bueno
                  and M.~{Garc\'{\i}a de la Banda} and K.~Marriott and
                  P.~J.~Stuckey},
  editor = {M.~Bruynooghe and K.~Lau},
  booktitle = {{P}rogram {D}evelopment in {C}omputational {L}ogic, {A}
                  {D}ecade of {R}esearch {A}dvances in {L}ogic-{B}ased
                  {P}rogram {D}evelopment},
  title = {{A} {G}eneric {F}ramework for {C}ontext-{S}ensitive
                  {A}nalysis of {M}odular {P}rograms},
  publisher = {Springer-Verlag},
  year = {2004},
  month = {August},
  series = {LNCS},
  number = {3049},
  pages = {234--261},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {anal},
  address = {Heidelberg, Germany},
  publisher_location = {Heidelberg, Germany},
  isbn = {3-540-22152-2},
  issn = {ISSN 0302-9743}
}

@incollection{preproc-disciplbook,
  author = {Germ\'an Puebla and F.~Bueno and M.~Hermenegildo},
  title = {{A} {G}eneric {P}reprocessor for {P}rogram {V}alidation and
                  {D}ebugging},
  editor = {P.~Deransart and M.~Hermenegildo and J.~Maluszynski},
  booktitle = {{A}nalysis and {V}isualization {T}ools for {C}onstraint
                  {P}rogramming},
  year = 2000,
  month = {September},
  pages = {63--107},
  npages = {45},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  series = {LNCS},
  number = {1870},
  butopics = {debug,lang,cons,anal},
  projects = {DISCIPL, DISCIPL-CICYT, EDIPIA}
}

@incollection{assert-lang-disciplbook,
  author = {Germ\'an Puebla and F.~Bueno and M.~Hermenegildo},
  title = {{A}n {A}ssertion {L}anguage for {C}onstraint {L}ogic
                  {P}rograms},
  editor = {P.~Deransart and M.~Hermenegildo and J.~Maluszynski},
  booktitle = {{A}nalysis and {V}isualization {T}ools for {C}onstraint
                  {P}rogramming},
  year = 2000,
  month = {September},
  pages = {23--61},
  npages = {39},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  series = {LNCS},
  number = {1870},
  butopics = {debug,lang,cons,anal},
  projects = {DISCIPL, DISCIPL-CICYT, EDIPIA}
}

@incollection{prog-glob-an,
  author = {M.~Hermenegildo and Germ\'an Puebla and F.~Bueno},
  title = {{U}sing {G}lobal {A}nalysis, {P}artial {S}pecifications,
                  and an {E}xtensible {A}ssertion {L}anguage for
                  {P}rogram {V}alidation and {D}ebugging},
  editor = {K.~R.~Apt and V.~Marek and M.~Truszczynski and
                  D.~S.~Warren},
  booktitle = {{T}he {L}ogic {P}rogramming {P}aradigm: a 25--{Y}ear
                  {P}erspective},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  butopics = {debug,lang,anal,spec},
  year = 1999,
  pages = {161--192},
  month = {July},
  projects = {DISCIPL, ELLA}
}

@incollection{ciao-novascience,
  author = {M.~Hermenegildo and F.~Bueno and D.~Cabeza and M.~Carro
                  and {M.~{Garc\'{\i}a de la Banda}} and
                  P.~L\'{o}pez-Garc\'{\i}a and Germ\'an Puebla},
  title = {{T}he {CIAO} {M}ulti-{D}ialect {C}ompiler and {S}ystem:
                  {A}n {E}xperimentation {W}orkbench for {F}uture
                  {(C)LP} {S}ystems},
  booktitle = {{P}arallelism and {I}mplementation of {L}ogic and
                  {C}onstraint {L}ogic {P}rogramming},
  pages = {65-85},
  publisher = {Nova Science},
  year = 1999,
  month = {April},
  address = {Commack, NY, USA},
  npages = 21,
  isbn = {ISBN 1-56072-673-3},
  butopics = {impl,lang,cons,anal,dist},
  projects = {ELLA, DISCIPL}
}

@inproceedings{hermenegildo11:ciao-stop,
  author = {M. V. Hermenegildo and F. Bueno and M. Carro and
              P. L\'{o}pez and E. Mera and J.F. Morales and Germ\'an Puebla},
  title = {{T}he {C}iao {A}pproach to the {D}ynamic vs. {S}tatic {L}anguage {D}ilemma},
  booktitle = {Proceedings for the International Workshop on Scripts to Programs, STOP'11},
  year = {2011},
  location = {Austin, Texas, USA},
  npages = {4},
  projects = {DOVES,HATS,PROMETIDOS,SCUBE},
  butopics = {lang,impl,autop,debug,env,anal,spec,gran},
  publisher = {ACM},
  address = {New York, NY, USA}
}

@inproceedings{tdg-lopstr10,
  author = {Elvira Albert and M.~G\'{o}mez-Zamalloa and J.M.~Rojas and Germ\'an Puebla},
  title = {Towards Compositional {CLP}-based Test Data Generation for Imperative Languages},
  booktitle = {20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'10)},
  year = {2010},
  month = {July},
  address = {Hagenberg, Austria},
  pages = {47--57},
  buconfj = {lopstr},
  butopics = {spec,anal},
  projects = {HATS,DOVES,PROMETIDOS},
  note = {Extended Abstract}
}

@inproceedings{AlbertGP10,
  author = {Elvira Albert and Miguel G\'{o}mez-Zamalloa and Germ{\'a}n Puebla},
  title = {{PET}: A {P}artial {E}valuation-based {T}est {C}ase {G}eneration {T}ool for {J}ava {B}ytecode},
  booktitle = {ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM'10)},
  year = {2010},
  pages = {25--28},
  isbn = {978-1-60558-727-1},
  publisher = {ACM Press}
}

Trust in software is typically achieved via stabilisation efforts over long periods of use. Adaptation to changing circumstances, however, often requires substantial change of the software. Changing a software system using standard manufacturing processes often results in quality regressions, invalidating trust. Formal methods provide means to guarantee various properties of a software system that increase its trustworthiness. The HATS methodology aims to integrate formal methods that model change through variability in and evolution of software systems, while preserving trustworthiness properties. This paper outlines how different formal methods are extended and integrated to build an industrially viable Software Product Line Engineering method for manufacturing highly adaptable and trustworthy software.

@inproceedings{ClarkeDHJPWW10,
  author = { Dave Clarke and Nikolay Diakov Reiner H{\"a}hnle and
                Einar Broch Johnsen and Germ{\'a}n Puebla and
                Balthasar Weitzel and Peter Y. H. Wong},
  title = {HATS---A Formal Software Product Line Engineering Methodology},
  booktitle = {1st International Workshop on Formal Methods in Software Product Line Engineering},
  year = {2010}
}

Cost functions provide information about the amount of resources required to execute a program in terms of the sizes of input arguments. They can provide an upper-bound, a lower-bound, or the average-case cost. Motivated by the existence of a number of automatic cost analyzers which produce cost functions, we propose an approach for automatically proving that a cost function is smaller than another one. In all applications of resource analysis, such as resource-usage verification, program synthesis and optimization, etc., it is essential to compare cost functions. This allows choosing an implementation with smaller cost or guaranteeing that the given resource-usage bounds are preserved. Unfortunately, automatically generated cost functions for realistic programs tend to be rather intricate, defined by multiple cases, involving non-linear subexpressions (e.g., exponential, polynomial and logarithmic) and they can contain multiple variables, possibly related by means of constraints. Thus, comparing cost functions is far from trivial. Our approach first syntactically transforms functions into simpler forms and then applies a number of sufficient conditions which guarantee that a set of expressions is smaller than another expression. Our preliminary implementation in the COSTA system indicates that the approach can be useful in practice.

@inproceedings{AlbertAGHP09,
  author = {Elvira Albert and Puri Arenas  and Samir Genaim and Israel Herraiz and Germ{\'a}n Puebla},
  title = {Comparing Cost Functions in Resource Analysis},
  booktitle = {International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA'09)},
  year = 2009,
  volume = 6324,
  pages = {1-17},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer}
}

COSTA is a research prototype which performs automatic program analysis and which is able to infer cost and termination information about Java bytecode programs. The system receives as input a bytecode program and a cost model chosen from a selection of resource descriptions, and tries to bound the resource consumption of the program with respect to the given cost model. COSTA provides several non-trivial notions of resource, such as the amount of memory allocated on the heap, the number of bytecode instructions executed, the number of billable events (such as sending a text message on a mobile phone) executed by the program. When performing cost analysis, COSTA produces a cost equation system, which is an extended form of recurrence relations. In order to obtain a closed (i.e., non-recursive) form for such recurrence relations which represents an upper bound, COSTA includes a dedicated solver. An interesting feature of COSTA is that it uses pretty much the same machinery for inferring upper bounds on cost as for proving termination (which also implies the boundedness of any resource consumption).

@inproceedings{AlbertAGPRZ08b,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Diana Ram\'irez and Damiano Zanardini},
  title = {Upper {B}ounds of {R}esource {U}sage for {J}ava {B}ytecode using {COSTA} and its {W}eb {I}nterface},
  booktitle = {Workshop on Resource Analysis},
  year = 2008,
  month = {September}
}

COSTA is a research prototype which performs automatic program analysis and which is able to infer cost and termination information about Java bytecode programs. The system receives as input a bytecode program and a cost model chosen from a selection of resource descriptions, and tries to bound the resource consumption of the program with respect to the given cost model. COSTA provides several non-trivial notions of resource, such as the amount of memory allocated on the heap, the number of bytecode instructions executed, the number of billable events (such as sending a text message on a mobile phone) executed by the program. When performing cost analysis, COSTA produces a cost equation system, which is an extended form of recurrence relations. In order to obtain a closed (i.e., non-recursive) form for such recurrence relations which represents an upper bound, COSTA includes a dedicated solver. An interesting feature of COSTA is that it uses pretty much the same machinery for inferring upper bounds on cost as for proving termination (which also implies the boundedness of any resource consumption).

@inproceedings{AlbertAGPRZ08a,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Diana Ram\'irez and Damiano Zanardini},
  title = {The {COSTA} {C}ost and {T}ermination {A}nalyzer for {J}ava {B}ytecode and its {W}eb {I}nterface ({T}ool {D}emo)},
  booktitle = {22nd European Conference on Object-Oriented Programming},
  year = 2008,
  editor = {Anna Philippou},
  month = {July}
}

Termination analysis tools strive to find proofs of termination for as wide a class of (terminating) programs as possible. Though several tools exist which are able to prove termination of non-trivial programs, when one tries to apply them to realistic programs, there are still a number of open problems. In the case of Java-like languages, one of such problems is to find a practical solution to prove termination when the termination behaviour of loops is affected by numeric fields. We have performed statistics on the Java libraries to see how often this happens in practice and we found that in 12.95% of cases, the number of iterations of loops (and therefore termination) explicitly depends on values stored in fields and, in the vast majority of cases, such fields are numeric. Inspired by the examples found in the libraries, this paper identifies a series of difficulties that need to be solved in order to deal with numeric fields in termination and propose some ideas towards a lightweight analysis which is able to prove termination of sequential Java-like programs in the presence of numeric fields.

@inproceedings{AlbertAGP08a,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla},
  title = {Dealing with Numeric Fields in Termination Analysis of Java-like Languages},
  booktitle = {10th Workshop on Formal Techniques for Java-like Programs},
  year = 2008,
  month = {July}
}

@inproceedings{AlbertAGPRZ08,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ\'an Puebla and
                  D.~Ram\'{\i}rez and D.~Zanardini},
  title = {The {\sc COSTA} Cost and Termination Analyzer for Java
  Bytecode and its Web Interface (Tool Demo)},
  booktitle = {22nd European Conference on Object-Oriented Programming
                  (ECOOP'08)},
  year = 2008,
  editor = {Anna Philippou},
  month = {July},
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {anal,gran}
}

@inproceedings{AlbertAGPZ08b,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ\'an Puebla and
                  D.~Zanardini},
  title = {{COSTA}: {A} {C}ost and {T}ermination {A}nalyzer for {J}ava
                  {B}ytecode},
  booktitle = {Proceedings of the Workshop on Bytecode Semantics,
                  Verification, Analysis and Transformation
                  (BYTECODE'08)},
  year = 2008,
  series = {Electronic Notes in Theoretical Computer Science},
  address = {Budapest, Hungary},
  month = {April},
  publisher = {Elsevier},
  note = {To appear},
  butopics = {anal,lang,gran},
  projects = {MOBIUS,MERIT,PROMESAS}
}

@article{oracle-pcpe-qapl08,
  author = {C.~Ochoa and Germ\'an Puebla},
  title = {{O}racle-{B}ased {P}oly-{C}ontrolled {P}artial {E}valuation},
  booktitle = {ETAPS Workshop on Quantitative Aspects of Programming
                  Languages (QAPL'08)},
  year = {2008},
  month = {March},
  journal = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
  volume = 220,
  number = 3,
  pages = {145--161},
  paper_presentation_city = {Budapest},
  paper_presentation_country = {Hungary},
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {spec,anal}
}

@inproceedings{Gomez-ZAP08b,
  author = {Miguel G\'{o}mez-Zamalloa and Elvira Albert and Germ{\'a}n Puebla},
  title = {{O}n the {G}eneration of {T}est {D}ata for {P}rolog by {P}artial {E}valuation},
  booktitle = {Workshop on Logic-based methods in Programming Environments (WLPE'08)},
  year = {2008},
  pages = {26--43}
}

@inproceedings{mod-decomp-prole08,
  author = {M. G\'{o}mez-Zamalloa and Elvira Albert and Germ\'an Puebla},
  title = {{T}owards {M}odular {I}nterpretive {D}ecompilation of {L}ow-{L}evel {C}ode to {P}rolog},
  booktitle = {8th Spanish Conference on Programming and Computer Languages (PROLE'08)},
  year = {2008},
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {spec,anal}
}

@inproceedings{jvm-cost-prole07,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ\'an Puebla and
                  D.~Zanardini},
  title = {A {G}eneric {F}ramework for the {C}ost {A}nalysis of {J}ava
                  {B}ytecode},
  booktitle = {Spanish Conference on
Programming and Computer Languages (PROLE'07)},
  year = {2007},
  month = {September},
  paper_presentation_city = {Zaragoza},
  paper_presentation_country = {Spain},
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {anal,debug,gran}
}

@inproceedings{typed-emb-lopstr07,
  author = {Elvira Albert and J.~Gallagher and M.~G\'{o}mez-Zamalloa and
                  Germ\'an Puebla},
  title = {{T}yped-based {H}omeomorphic {E}mbedding for {O}nline
                  {T}ermination},
  booktitle = {17th International Symposium on Logic-based Program
                  Synthesis and Transformation (LOPSTR'07)},
  year = {2007},
  month = {August},
  projects = {MOBIUS,MERIT,PROMESAS,noimdea},
  butopics = {spec,anal},
  note = {Extended Abstract}
}

@inproceedings{assert-pe-bytecode07,
  author = {M. G\'{o}mez-Zamalloa and Elvira Albert and Germ\'an Puebla},
  title = {{I}mproving the {D}ecompilation of {J}ava {B}ytecode to
                  {P}rolog
                 by {P}artial {E}valuation},
  booktitle = {ETAPS Workshop on Bytecode Semantics, Verification,
                 Analysis and Transformation (BYTECODE'07)},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {{E}lsevier - {N}orth {H}olland},
  editor = {M. Huisman and F. Spoto},
  pages = {85-101},
  volume = {190, Issue 1},
  year = {2007},
  month = {July},
  paper_presentation_city = {Braga},
  paper_presentation_country = {Portugal},
  projects = {MOBIUS,MERIT,PROMESAS,POAIST},
  butopics = {spec,anal}
}

@incollection{pcpe-wflp-entcs,
  author = {C.~Ochoa and Germ\'an Puebla},
  title = {{A} {S}tudy on the {P}racticality of {P}oly-{C}ontrolled
                  {P}artial {E}valuation},
  series = {Electronic Notes in Theoretical Computer Science},
  booktitle = {Proceedings of the 15th Workshop on Functional and
                  (Constraint) Logic Programming (WFLP'06)},
  month = {June},
  year = 2007,
  publisher = {{E}lsevier},
  volume = 177,
  pages = {137-151},
  npages = 15,
  butopics = {anal,spec},
  projects = {MOBIUS,MERIT,PROMESAS},
  foo = {http://www.sciencedirect.com/science/journal/15710661}
}

In this abstract, we discuss several aspects of the role of static slicing to minimize the number of arguments which need to be taken into account in CES. We will focus on two benefits of eliminating the arguments which do not have an impact on the cost of the program. On one hand, analysis can be more efficient if we reduce the number of variables. And also CES are more likely to be solved by standard CAS.

@inproceedings{AlbertAGPZ07c,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'a}n Puebla and Damiano Zanardini},
  title = {{A}pplications of {S}tatic {S}licing in {C}ost {A}nalysis of {J}ava {B}ytecode},
  booktitle = {The 3rd International Workshop on Programming Language Interference and Dependence (PLID'07) ,Kongens Lyngby, Denmark, 21 August, 2007},
  year = 2007
}

In this work, we describe a termination analysis for Java bytecode, based on a translation into a structured intermediate representation. This representation captures in a uniform setting all loops (regardless of whether they originate from recursive calls or iterative loops) and all variables (either local variables or operand stack elements). Given this representation we consider a general form of the size-change graphs principle to prove termination of the intermediate program, which in turn implies the termination of the original program.

@inproceedings{AlbertACGPZ07,
  author = {Elvira Albert and Puri Arenas and Michael Codish and Samir Genaim and Germ{\'a}n Puebla and Damiano Zanardini},
  title = {{T}ermination {A}nalysis of {J}ava {B}ytecode},
  booktitle = {Proceedings of the 9th International Workshop on Termination, WST'07 Paris, France, June 29, 2007},
  editor = {Alexander Serebrenik and Dieter Hofbauer},
  year = 2007
}

@inproceedings{jvm-cost-exp-bytecode07,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Germ\'an Puebla and
                  D.~Zanardini},
  title = {{E}xperiments in {C}ost {A}nalysis of {J}ava {B}ytecode},
  booktitle = {ETAPS Workshop on Bytecode Semantics, Verification,
                 Analysis and Transformation (BYTECODE'07)},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
  year = {2007},
  volume = {190, Issue 1},
  paper_presentation_city = {Braga},
  paper_presentation_country = {Portugal},
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {anal,debug,gran}
}

@inproceedings{ai-safety-reduced-prole06,
  author = {Elvira Albert and Puri Arenas and Germ\'an Puebla and M. Hermenegildo},
  title = {Generation of {R}educed {C}ertificates in
                 {A}bstraction-{C}arrying {C}ode},
  booktitle = {VI Jornadas Programaci\'on y Lenguajes (PROLE'06)},
  year = {2006},
  month = {October},
  npages = 10,
  projects = {MERIT,MOBIUS,POAIST,PROMESAS},
  butopics = {anal,debug}
}

@inproceedings{estim-exec-time-wlpe,
  author = {E.~Mera and P. L\'{o}pez-Garc\'{\i}a and Germ\'an Puebla and
                  M.~Carro and M. Hermenegildo},
  title = {{T}owards {E}xecution {T}ime {E}stimation for {L}ogic
                  {P}rograms via {S}tatic {A}nalysis and {P}rofiling},
  booktitle = {16th Workshop on Logic Programming Environments},
  pages = {45--60},
  year = 2006,
  editor = {S. Mu\~{n}oz and W. Vanhoof},
  month = {August},
  publisher = {University of Namur, Institut d'Informatique},
  projects = {MOBIUS,MERIT,PROMESAS,POAIST},
  butopics = {anal,gran}
}

@inproceedings{inc-acc-wlpe06,
  author = {Elvira Albert and Puri Arenas and Germ\'an Puebla},
  title = {Some {I}ssues on {I}ncremental {A}bstraction-{C}arrying
                  {C}ode},
  booktitle = {16th Workshop on Logic-Based Methods in Programming
                  Environments (WLPE'06) },
  year = 2006,
  month = {August},
  npages = 15,
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {anal,debug}
}

@inproceedings{jvm-by-pe-svv06,
  author = {Elvira Albert and M. G\'{o}mez-Zamalloa and L. Hubert and
                  Germ\'an Puebla},
  title = {Towards {V}erification of {J}ava {B}ytecode using {T}ools
                  for {L}ogic {P}rogramming},
  booktitle = {International Workshop on Software Verification and
                  Validation (SVV 2006)},
  year = 2006,
  month = {August},
  npages = 15,
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {anal,debug}
}

@inproceedings{inc-acc-wits06,
  author = {Elvira Albert and Puri Arenas and Germ\'an Puebla},
  title = {Incremental {C}ertificates and {C}heckers for
{A}bstraction-{C}arrying {C}ode},
  booktitle = {Sixth Workshop on Issues in the Theory of Security},
  year = 2006,
  month = {March},
  npages = 16,
  projects = {MOBIUS,MERIT,PROMESAS},
  butopics = {anal,debug}
}

@inproceedings{ai-with-specs-wlpe05,
  author = {Germ\'an Puebla and Elvira Albert and M.~Hermenegildo},
  title = { A {G}eneric {F}ramework for the {A}nalysis and
                  {S}pecialization of {L}ogic {P}rograms },
  booktitle = {The 15th Workshop on Logic-Based Methods in Programming
               Environments, WLPE'05},
  npages = 15,
  year = 2005,
  month = {October},
  address = {Sitges (Barcelona)},
  paper_presentation_city = {Sitges (Barcelona)},
  paper_presentation_country = {Spain},
  butopics = {anal,spec},
  projects = {CUBICO, ASAP, POAIST}
}

@inproceedings{wil04-backwards,
  author = {Elvira Albert and Germ\'an Puebla and J.~Gallagher},
  title = {A {P}artial {D}educer {A}ssisted by {P}redefined
                  {A}ssertions and a
   {B}ackwards {A}nalyzer},
  booktitle = {5th International Workshop on the Implementation of
                  Logics (WIL'04)},
  year = {2005},
  month = {March},
  npages = 9,
  paper_presentation_city = {Montevideo},
  paper_presentation_country = {Uruguay},
  projects = {ASAP,CUBICO},
  butopics = {anal,spec}
}

@inproceedings{sonda04-ai-safety,
  author = {Elvira Albert and Germ\'an Puebla and M.~Hermenegildo},
  title = {{A}bstract {I}nterpretation-based {C}ode
  {C}ertification for {P}ervasive {S}ystems: {P}reliminary
                  {E}xperiments},
  booktitle = {Workshop on Software Analysis and Development for
Pervasive Systems (SONDA'04)},
  year = {2004},
  month = {August},
  npages = 6,
  pages = {1--6},
  paper_presentation_city = {Verona},
  paper_presentation_country = {Italy},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {anal,debug}
}

@inproceedings{lopstr04-unfolding-informal,
  author = {Germ\'an Puebla and Elvira Albert},
  title = {Efficient {L}eftmost {U}nfolding with {A}ncestor {S}tacks},
  booktitle = {Pre-proceedings of the 14th International Symposium on
                  Logic-based Program Synthesis and Transformation
                  (LOPSTR'04)},
  year = {2004},
  month = {August},
  paper_presentation_city = {Verona},
  paper_presentation_country = {Italy},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {spec}
}

@inproceedings{cocv04-ai-safety,
  author = {Elvira Albert and Germ\'an Puebla and M.~Hermenegildo},
  title = {An {A}bstract {I}nterpretation-based {A}pproach to {M}obile
                  {C}ode {S}afety},
  booktitle = {Proc. of Compiler Optimization meets Compiler
                  Verification (COCV'04)},
  series = {Electronic Notes in Theoretical Computer Science 132(1)},
  publisher = {{E}lsevier - {N}orth {H}olland},
  pages = {113-129},
  year = {2004},
  month = {April},
  paper_presentation_city = {Barcelona},
  paper_presentation_country = {Spain},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {anal,debug},
  buconfj = {cocv}
}

@inproceedings{modular-anal-lopstr-informal,
  author = {F.~Bueno and M.~{Garcia de la Banda} and M.~Hermenegildo
                  and
                 K.~Marriott and Germ\'an Puebla and P.~Stuckey},
  title = {A Model for Inter-module Analysis and Optimizing
                  Compilation},
  booktitle = {Tenth International Workshop on
         Logic-based Program Synthesis and Transformation},
  year = 2000,
  month = {July},
  butopics = {anal,spec},
  projects = {EDIPIA}
}

@incollection{ciao-modules-analspec-entcs,
  author = {Germ\'an Puebla and M.~Hermenegildo},
  title = {{S}ome {I}ssues in {A}nalysis and {S}pecialization of
                  {M}odular {C}iao-{P}rolog {P}rograms},
  series = {Electronic Notes in Theoretical Computer Science},
  booktitle = {Special Issue on Optimization and Implementation of
                  Declarative Programming Languages},
  month = {March},
  year = 2000,
  publisher = {{E}lsevier - {N}orth {H}olland},
  volume = 30,
  number = 2,
  npages = 25,
  butopics = {anal,spec,impl},
  projects = {ELLA, DISCIPL, DISCIPL-CICYT},
  foo = {http://www.elsevier.com/locate/entcs/volume30.html}
}

@inproceedings{pe-in-plai-pepm99,
  author = {Germ\'an Puebla and M.~Hermenegildo and J.~Gallagher},
  title = {{A}n {I}ntegration of {P}artial {E}valuation in a {G}eneric
                  {A}bstract {I}nterpretation {F}ramework},
  booktitle = {ACM SIGPLAN Workshop on Partial Evaluation and
                  Semantics-Based Program Manipulation (PEPM'99)},
  year = 1999,
  editor = {O~Danvy},
  month = {January},
  publisher = {University of Aarhus, Denmark},
  series = {BRISC Series},
  number = {NS-99-1},
  pages = {75--85},
  paper_presentation_city = {San Antonio, Texas},
  paper_presentation_country = {USA},
  butopics = {spec,anal},
  buconfj = {pepm},
  projects = {DISCIPL, ELLA}
}

@inproceedings{assrt-framework-jicslp98ws,
  author = {Germ\'an Puebla and F.~Bueno and M.~Hermenegildo},
  title = {{A} {F}ramework for {A}ssertion-based {D}ebugging in
                  {C}onstraint {L}ogic {P}rogramming},
  booktitle = {Proceedings of the JICSLP'98 Workshop on Types for
                  CLP},
  year = {1998},
  month = {June},
  address = {Manchester, UK},
  pages = {3--15},
  butopics = {debug,anal},
  paper_presentation_city = {Manchester},
  paper_presentation_country = {UK},
  projects = {ELLA, DISCIPL}
}

@inproceedings{assert-lang-ws,
  author = {Germ\'an Puebla and F.~Bueno and M.~Hermenegildo},
  title = {{A}n {A}ssertion {L}anguage for {D}ebugging of {C}onstraint
                  {L}ogic {P}rograms},
  booktitle = {Proceedings of the ILPS'97 Workshop on Tools and
                  Environments for (Constraint) Logic Programming},
  year = 1997,
  month = {October},
  note = {Available from \htmladdnormallink{{\tt
    ftp://clip.dia.fi.upm.es/pub/papers/assert\_lang\_tr\_discipldeliv.ps.gz}}
   {ftp://clip.dia.fi.upm.es/pub/papers/assert\_lang\_tr\_discipldeliv.ps.gz}
                  as technical report {CLIP}2/97.1.},
  paper_presentation_city = {Port Jefferson, NY},
  paper_presentation_country = {USA},
  butopics = {debug,lang,anal,cons}
}

@inproceedings{pe-in-plai-ws,
  author = {Germ\'an Puebla and J.~Gallagher and M.~Hermenegildo},
  title = {{T}owards {I}ntegrating {P}artial {E}valuation in a
                  {S}pecialization {F}ramework based on {G}eneric
                  {A}bstract {I}nterpretation},
  booktitle = {Proceedings of the ILPS'97 Workshop on Specialization
                  of Declarative Programs},
  year = 1997,
  editor = {M.~Leuschel},
  month = {October},
  note = {Post ILPS'97 Workshop},
  paper_presentation_city = {Port Jefferson, NY},
  paper_presentation_country = {USA},
  butopics = {spec,anal}
}

@inproceedings{spec-dyn-sch-waill97,
  author = {Germ\'an Puebla and M.~{Garc\'{\i}a de la Banda} and
                  M.~Hermenegildo and K.~Marriott and P.~Stuckey},
  title = {Automatic {O}ptimization of {L}ogic {P}rograms with
                  {D}ynamic {S}cheduling},
  booktitle = {Workshop on Abstract Interpretation of Logic
                  Languages},
  year = {1996},
  month = {December},
  publisher = {The Hebrew University},
  address = {Jerusalem},
  butopics = {conc,anal,spec}
}

@inproceedings{ciao-jicslp96-ws-update,
  author = {M.~Hermenegildo and F.~Bueno and D.~Cabeza and M.~Carro
                  and M.~{Garc\'{\i}a de la Banda} and
                  P.~L\'{o}pez-Garc\'{\i}a and Germ\'an Puebla},
  title = {{T}he {CIAO} {M}ulti-{D}ialect {C}ompiler and {S}ystem: {A}
                  {D}emo and {S}tatus {R}eport},
  booktitle = {Proceedings of the JICSLP'96 Workshop on Parallelism
                  and Implementation Technology},
  year = {1996},
  month = {September},
  publisher = {Computer Science Department, Technical University of
                  Madrid},
  note = {Available from \htmladdnormallink{{\tt
                  http://www.cliplab.org/Projects/COMPULOG/meeting96/papers/PS/clip.ps.gz}}
                  {http://www.cliplab.org/Projects/COMPULOG/meeting96/papers/PS/clip.ps.gz}},
  url = {http://www.cliplab.org/Projects/COMPULOG/meeting96/papers/PS/clip.ps.gz},
  butopics = {impl,anal,lang,cons},
  projects = {PRINCE, PARFORCE, ACCLAIM, IPL-D},
  publisher_location = {Madrid, Spain},
  paper_presentation_city = {Bonn},
  paper_presentation_country = {Germany},
  npages = {12}
}

@inproceedings{inc-fixp-ws,
  author = {Germ\'an Puebla and M.~Hermenegildo},
  title = {{O}ptimized {A}lgorithms for the {I}ncremental {A}nalysis
                  of {L}ogic {P}rograms},
  booktitle = {II Workshop on Verification and Analysis of Logic
                  Languages},
  year = {1996},
  month = {September},
  paper_presentation_city = {Bonn},
  paper_presentation_country = {Germany},
  butopics = {anal}
}

@inproceedings{ciao-prolog-prode-full,
  author = {M. Hermenegildo and F.~Bueno and D.~Cabeza and M.~Carro
                  and M.~{Garc\'{\i}a de la Banda} and P.~L\'{o}pez and
                  Germ\'an Puebla},
  title = {{T}he {CIAO} {M}ulti-{D}ialect {C}ompiler and {S}ystem:
                  {A}n {E}xperimentation {W}orkbench for {F}uture
                  {(C)LP} {S}ystems},
  booktitle = {Proc. of the AGP'96 Joint Conference on Declarative
                  Programming},
  pages = {105--108},
  year = {1996},
  month = {July},
  publisher = {U.\ of the Basque Country},
  address = {San Sebastian, Spain},
  note = {Available from {\tt ftp://www.cliplab.org/pub/papers}},
  paper_presentation_city = {San Sebastian},
  paper_presentation_country = {Spain},
  publisher_location = {Spain},
  butopics = {impl,lang,cons,anal}
}

@inproceedings{abs-exec-meta96,
  author = {Germ\'an Puebla and M.~Hermenegildo},
  editor = {J.~Gallagher},
  title = {{A}bstract {S}pecialization and its {A}pplication to
                  {P}rogram {P}arallelization},
  booktitle = {V International Workshop on Metaprogramming and
                  Metareasoning in Logic},
  year = {1996},
  butopics = {autop,spec,anal}
}

@inproceedings{ciao-ilps95,
  author = {M. Hermenegildo and F. Bueno and M.~Garc\'{\i}a de la
                  Banda and Germ\'an Puebla},
  title = {{T}he {CIAO} {M}ulti-{D}ialect {C}ompiler and {S}ystem:
                  {A}n {E}xperimentation {W}orkbench for {F}uture
                  {(C)LP} {S}ystems},
  booktitle = {Proceedings of the ILPS'95 Workshop on Visions for the
                  Future of Logic Programming},
  year = {1995},
  month = {December},
  address = {Portland, Oregon, USA},
  note = {Available from \htmladdnormallink{{\tt
                  http://www.cliplab.org/}}
                  {http://www.cliplab.org/}},
  butopics = {impl,lang,cons,anal},
  projects = {PRINCE, PARFORCE, ACCLAIM, IPL-D}
}

@inproceedings{ICLPWSanal,
  author = {F.~Bueno and D.~Cabeza and M.~Hermenegildo and Germ\'an Puebla},
  title = {{D}ata--flow {A}nalysis of {S}tandard {P}rolog {P}rograms},
  booktitle = {ICLP95 WS on Abstract Interpretation of Logic
                  Languages},
  year = 1995,
  month = {June},
  address = {Japan},
  butopics = {anal},
  projects = {PARFORCE, IPL-D}
}

@book{pepm09,
  author = {Germ\'an Puebla and G.~Vidal},
  title = {ACM SIGPLAN Partial Evaluation and Program Manipulation
                  (PEPM'09)},
  publisher = {ACM Digital Library},
  year = 2009,
  month = {January},
  butopics = {misc},
  npages = {200},
  isbn = {ISBN 978-1-60558-327-3},
  buconfj = {pepm},
  projects = {MOBIUS,MERIT,PROMESAS}
}

@book{lopstr06,
  author = {Germ\'an Puebla},
  title = {Logic Based Program Synthesis and Transformation
                  (LOPSTR'06)},
  publisher = {Springer},
  year = 2007,
  month = {March},
  number = 4407,
  series = {LNCS},
  butopics = {misc},
  npages = {237},
  isbn = {ISBN 978-3-540-71409-5},
  buconfj = {lopstr},
  projects = {MOBIUS,MERIT,PROMESAS}
}

@book{sas02,
  title = {{S}tatic {A}nalysis -- 9th. {I}nternational {S}ymposium},
  year = 2002,
  month = {September},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  address = {Heidelberg, Germany},
  number = {2477},
  series = {LNCS},
  npages = {528},
  author = {M. Hermenegildo and Germ\'an Puebla},
  butopics = {misc},
  buconfj = {sas},
  isbn = {ISBN 3-540-44235-9},
  issn = {ISSN 0302-9743}
}

@phdthesis{german-phd,
  author = {Germ\'an Puebla},
  title = {{A}dvanced {C}ompilation {T}echniques based on {A}bstract
                  {I}nterpretation and {P}rogram {T}ransformation},
  year = 1997,
  month = {November},
  address = {Facultad Informatica UPM, 28660-Boadilla del Monte,
                  Madrid-Spain},
  school = {Universidad Polit\'{e}cnica de Madrid (UPM)},
  butopics = {anal,spec,autop,debug}
}

@proceedings{tools-env-ws,
  title = {{P}roceedings of the {ILPS'97} {W}orkshop on {T}ools and
                  {E}nvironments for {C}onstraint {L}ogic
                  {P}rogramming},
  editor = {Germ\'an Puebla and M.~Comini and W.~Drabent and M.~Ducasse and
                  M.~Fabris and M.~Meier and Ch.~Schulte},
  author = {Germ\'an Puebla and M.~Comini and W.~Drabent and M.~Ducasse and
                  M.~Fabris and M.~Meier and Ch.~Schulte},
  year = {1997},
  month = {October},
  number = {CLIP7/97.1},
  npages = {180},
  publisher = {Facultad de Inform\'atica, UPM},
  publisher_location = {Madrid, Spain},
  institution = {Technical University of Madrid (UPM)},
  type = {Technical Report},
  butopics = {misc},
  url = {http://cliplab.org/Tools_Environ/call_for_papers.html}
}

@mastersthesis{german-master,
  author = {Germ\'an Puebla},
  title = {{S}implification and {S}pecialization of {L}ogic {P}rograms
                  based on {A}bstract {I}nterpretation},
  year = 1994,
  month = {January},
  school = {School of Computer Science. Technical University of
                  Madrid},
  note = {(in Spanish)},
  butopics = {anal,spec}
}

@inproceedings{Albert-LPAR18-invited,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and M. G\'omez-Zamalloa and G.~Puebla},
  title = {Automatic {I}nference of {R}esource {C}onsumption {B}ounds},
  booktitle = {18th International Conference on
Logic for Programming, Artificial Intelligence, and
Reasoning (LPAR-18)},
  publisher = {Springer},
  butopics = {anal,verif},
  buconfj = {pepm},
  projects = {HATS,PROMETIDOS,DOVES},
  year = {2012},
  month = {March},
  note = {To appear}
}

@inproceedings{tutorial-ruleml11,
  author = {M.~V.~Hermenegildo and F. Bueno and M. Carro and P.~L\'{o}pez-Garc\'{\i}a and 
            R. Haemmerl\'{e} and E. Mera and J. F. Morales and Germ\'an Puebla},
  title = {{A}n {O}verview of the {C}iao {S}ystem},
  booktitle = {Proc. of {RuleML-Europe 2011}},
  buconfj = {ruleml},
  year = 2011,
  month = {July},
  publisher = {Springer-Verlag},
  editor = {N. Bassiliades et al.},
  series = {LNCS},
  number = 6826,
  pages = {2--3},
  note = {(abstract of invited talk)}
}

@inproceedings{pcc-scenarios-fmco07,
  author = {Germ\'an Puebla},
  title = {Scenarios for {P}roof {C}arrying {C}ode},
  booktitle = {Formal Methods for Components and Objects, FMCO'2007},
  year = 2007,
  month = {November},
  butopics = {debug,anal},
  projects = {MOBIUS,PROMESAS,MERIT},
  buconfj = {fmco},
  paper_presentation_city = {Amsterdam},
  paper_presentation_country = {The Netherlands}
}

@inproceedings{mobius-tgc06,
  author = {G.~Barthe and L.~Beringer and P.~Cr\'egut and
                  B.~Gr\'egoire and M.~Hofmann and P.~M{\"u}ller and
                  E.~Poll and Germ\'an Puebla and I.~Stark and
                  E.~V\'etillard},
  title = {MOBIUS: Mobility, Ubiquity, Security: Objectives and
                  progress report},
  booktitle = {Trustworthy Global Computing'06},
  year = 2007,
  month = {March},
  publisher = {Springer},
  series = {LNCS},
  projects = {MOBIUS,MERIT,PROMESAS,noimdea},
  butopics = {anal,debug},
  number = {4661},
  pages = {10--29},
  buconfj = {tgc},
  isbn = {978-3-540-75333-9}
}

@inproceedings{sac06,
  author = {M.~Hermenegildo and Elvira Albert and Puri Arenas and F. Bueno
               and P. Lopez-Garcia and M.~M\'{e}ndez-Lojo and
                  Germ\'an Puebla},
  title = {{A}dvanced {P}rogram {D}evelopment {U}sing {A}bstract
                  {I}nterpretation},
  booktitle = {ACM SAC'06, ACM Symposium in Applied Computing (keynote
                  address)},
  year = 2006,
  month = {April},
  buconfj = {sac},
  butopics = {anal,spec,gran,debug,impl,env},
  projects = {MOBIUS,MERIT,PROMESAS,POAIST},
  paper_presentation_city = {Dijon},
  paper_presentation_country = {France}
}

@inproceedings{ai-safety-reduced-eaai05,
  author = {Germ\'an Puebla and Elvira Albert and Puri Arenas and M.~Hermenegildo},
  title = {On {A}bstraction-{C}arrying {C}ode and {C}ertificate-{S}ize
                  {R}eduction},
  booktitle = {1st International Workshop on Emerging Applications of
                 Abstract Interpretation (EAAI 2006)},
  year = {2006},
  month = {March},
  npages = 15,
  paper_presentation_city = {Viena},
  paper_presentation_country = {Austria},
  projects = {MOBIUS,MERIT,PROMESAS,POAIST},
  butopics = {anal,debug}
}

@inproceedings{damp06,
  author = {M.~Hermenegildo and F.~Bueno and D.~Cabeza and M.~Carro
               and A.~Casas and P.~L\'{o}pez-Garc\'{\i}a and
                  Germ\'an Puebla},
  title = {{A}utomatic {P}arallelization of {L}ogic and {C}onstraint
                  {P}rograms},
  booktitle = {DPMC, Intel Workshop on Declarative Programming
                  Languages for Multicore Programming},
  year = 2006,
  month = {January},
  butopics = {autop,gran},
  projects = {MOBIUS,MERIT,PROMESAS,POAIST},
  paper_presentation_city = {Charleston, SC},
  paper_presentation_country = {U.S.A.}
}

@inproceedings{ai-safety-movelog05,
  author = {Germ\'an Puebla and Elvira Albert and M. Hermenegildo},
  title = {Abstract {I}nterpretation-based
                  {V}erification/{C}ertification in the {C}iaoPP
                  {S}ystem},
  booktitle = { Mobile Code Safety and Program Verification Using
                  Computational Logic Tools (MoveLog'05)},
  year = {2005},
  month = {October},
  npages = 9,
  paper_presentation_city = {Sitges},
  paper_presentation_country = {Spain},
  projects = {ASAP,CUBICO,MOBIUS},
  butopics = {anal,debug},
  buconfj = {movelog}
}

@inproceedings{acc-res-ppdp05-long,
  author = {M.~Hermenegildo and Elvira Albert and P.~L\'{o}pez-Garc\'{\i}a
                  and Germ\'an Puebla},
  title = {{A}bstraction {C}arrying {C}ode and
                  {R}esource-{A}wareness},
  booktitle = {7th ACM-SIGPLAN International Symposium on
                 Principles and Practice of Declarative Programming
                  (PPDP'05)},
  year = {2005},
  month = {July},
  pages = {1-11},
  publisher = {ACM Press},
  paper_presentation_city = {Lisbon},
  paper_presentation_country = {Portugal},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {anal,debug,gran},
  buconfj = {ppdp}
}

@inproceedings{tutorial-europar04,
  author = {M.~Hermenegildo and Elvira Albert and P.~L\'{o}pez-Garc\'{\i}a
                  and Germ\'an Puebla},
  title = {Some {T}echniques for {A}utomated, {R}esource-{A}ware
                  {D}istributed and {M}obile {C}omputing in a
                  {M}ulti-{P}aradigm {P}rogramming {S}ystem},
  booktitle = {Proc. of {EURO--PAR 2004}},
  year = {2004},
  month = {August},
  paper_presentation_city = {Pisa},
  paper_presentation_country = {Italy},
  publisher = {Springer-Verlag},
  series = {LNCS},
  number = {3149},
  pages = {21--37},
  projects = {ASAP,CUBICO,POAIST},
  butopics = {anal,debug,gran},
  buconfj = {europar},
  isbn = {ISBN 3-540-22924-8},
  issn = {ISSN 0302-9743}
}

@inproceedings{spec-inv-pepm03,
  author = {Germ\'an Puebla and M.~Hermenegildo},
  title = {{A}bstract {S}pecialization and its {A}pplications},
  booktitle = {ACM Partial Evaluation and Semantics based Program
                  Manipulation (PEPM'03)},
  year = 2003,
  month = {June},
  note = {Invited talk},
  pages = {29--43},
  publisher = {{ACM} {P}ress},
  butopics = {spec,anal},
  buconfj = {pepm},
  projects = {ASAP, CUBICO, ADELA},
  paper_presentation_city = {San Diego, California},
  paper_presentation_country = {USA},
  publisher_location = {NY, USA},
  isbn = {ISBN 1-58113-667-6}
}

@inproceedings{ciaopp-sas03,
  author = {M.~Hermenegildo and Germ\'an Puebla and F.~Bueno and
                  P.~L\'{o}pez-Garc\'{\i}a},
  title = {{P}rogram {D}evelopment {U}sing {A}bstract {I}nterpretation
                  (and {T}he {C}iao {S}ystem {P}reprocessor)},
  booktitle = {10th {I}nternational {S}tatic {A}nalysis {S}ymposium
                  (SAS'03)},
  year = {2003},
  month = {June},
  pages = {127--152},
  number = {2694},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  series = {LNCS},
  butopics = {anal,spec,autop,gran,debug,impl,env},
  buconfj = {sas},
  paper_presentation_city = {San Diego, CA},
  paper_presentation_country = {USA},
  projects = {CUBICO, EDIPIA, ADELA, ASAP},
  isbn = {3-540-40325-6},
  issn = {ISSN 0302-9743}
}

@inproceedings{assrt-framework-ercim02,
  author = {M.~Hermenegildo and Germ\'an Puebla and F.~Bueno and
                  P.~L\'{o}pez-Garc\'{\i}a},
  title = {{A}bstract {V}erification and {D}ebugging of {C}onstraint
                  {L}ogic {P}rograms},
  booktitle = {Recent Advances in Constraints},
  year = {2003},
  month = {January},
  pages = {1--14},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  series = {LNCS},
  number = {2627},
  butopics = {debug,anal},
  paper_presentation_city = {Cork},
  paper_presentation_country = {Ireland},
  projects = {EDIPIA,ASAP,CUBICO,ADELA},
  issn = {ISSN 0302-9743}
}

@inproceedings{assrt-framework-icalp02,
  author = {M.~Hermenegildo and F.~Bueno and Germ\'an Puebla and
                  P.~L\'{o}pez-Garc\'{\i}a},
  title = {{P}rogram {D}ebugging and {V}alidation {U}sing {S}emantic
                  {A}pproximations and {P}artial {S}pecifications},
  booktitle = {29 th.\ {I}nternational {C}olloqium on {A}utomata,
                  {L}anguages, and {P}rogramming ({ICALP})},
  year = {2002},
  month = {July},
  pages = {69--72},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  series = {LNCS},
  number = {2380},
  butopics = {debug,anal},
  buconfj = {icalp},
  paper_presentation_city = {Malaga},
  paper_presentation_country = {Spain},
  projects = {EDIPIA, ASAP},
  issn = {ISSN 0302-9743}
}

@inproceedings{agents-ciao-epia01,
  author = {F.~Bueno and D.~Cabeza and M.~Carro and Jes\'us Correas and
            J.~G\'{o}mez and M.~Hermenegildo and P.~L\'{o}pez and
            Germ\'an Puebla and C.~Vaucheret},
  title = {{A}gent {P}rogramming in {C}iao {P}rolog},
  booktitle = {10 th.\ {P}ortuguese {C}onference on {A}rtificial
                  {I}ntelligence ({EPIA})},
  year = {2001},
  month = {December},
  npages = {2},
  publisher = {Springer-Verlag},
  publisher_location = {Heidelberg, Germany},
  series = {LNAI},
  number = 2258,
  butopics = {dist,lang,misc},
  paper_presentation_city = {Porto},
  paper_presentation_country = {Portugal},
  projects = {EDIPIA},
  issn = {ISSN 0302-9743}
}

@inproceedings{ciao-cl2000-tut,
  author = {M.~Hermenegildo and F.~Bueno and D.~Cabeza and M.~Carro
                  and
               M.~{Garc\'{\i}a de la Banda} and
                  P.~L\'{o}pez-Garc\'{\i}a
               and Germ\'an Puebla},
  title = {{T}he {C}iao {L}ogic {P}rogramming {E}nvironment: {A}
                  {T}utorial},
  booktitle = {International Conference on Computational Logic,
                  CL2000},
  year = 2000,
  month = {July},
  buconfj = {cl},
  butopics = {impl,debug,anal,lang,cons,gran},
  projects = {EDIPIA},
  paper_presentation_city = {London},
  paper_presentation_country = {U.K.}
}

@inproceedings{ciaopp-iclp99-tut,
  author = {M.~Hermenegildo and F.~Bueno and Germ\'an Puebla and
                  P.~L\'{o}pez-Garc\'{\i}a},
  title = {{P}rogram {A}nalysis, {De}bugging and {O}ptimization
                  {U}sing the {C}iao {S}ystem {P}reprocessor},
  booktitle = {1999 Int'l. Conference on Logic Programming},
  year = {1999},
  month = {November},
  pages = {52--66},
  publisher = {MIT Press},
  address = {Cambridge, MA},
  publisher_location = {Cambridge, MA, USA},
  butopics = {impl,debug,anal,lang,cons,gran},
  buconfj = {iclp},
  paper_presentation_city = {Las Cruces, NM},
  paper_presentation_country = {USA},
  projects = {ELLA, DISCIPL}
}

@inproceedings{aadebug97-informal,
  author = {F.~Bueno and P.~Deransart and W.~Drabent and G.~Ferrand
                  and M.~Hermenegildo and J.~Maluszynski and
                  Germ\'an Puebla},
  title = {{O}n the {R}ole of {S}emantic {A}pproximations in
                  {V}alidation and {D}iagnosis of {C}onstraint {L}ogic
                  {P}rograms},
  booktitle = {Proc.\ of the 3rd. Int'l Workshop on Automated
                  Debugging--AADEBUG'97},
  pages = {155--170},
  year = {1997},
  month = {May},
  publisher = {U.\ of Link\"oping Press},
  address = {Link\"oping, Sweden},
  url = {ftp://clip.dia.fi.upm.es/pub/papers/aadebug_discipldeliv.ps.gz},
  butopics = {debug,anal,cons},
  paper_presentation_city = {Link\"oping},
  paper_presentation_country = {Sweden},
  publisher_location = {Sweden},
  projects = {DISCIPL}
}

@inproceedings{dagstuhl-abstract,
  author = {M.~Hermenegildo and Germ\'an Puebla},
  editor = {O.~Danvy and R.~Glueck and P.~Thiemann},
  title = {{A}pplying {M}ultiple {A}bstract {S}pecialization to
                  {P}rogram {P}arallelization (abstract)},
  booktitle = {Partial Evaluation-- Dagstuhl Seminar Report},
  year = {1996},
  month = {February},
  npages = {1},
  publisher = {IBFI -- Dagstuhl},
  number = {134},
  butopics = {autop,spec}
}