The aim of incremental 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. The first contribution of this article is a multi-domain incremental fixed-point algorithm for a sequential Java-like language. The algorithm is multi-domain in the sense that it interleaves the (re-)analysis for multiple domains by taking into account dependencies among them. Importantly, this allows the incremental analyzer to invalidate only those analysis results previously inferred by certain dependent domains. The second contribution is an incremental resource usage analysis which, in its first phase, uses the multi-domain incremental fixed-point algorithm to carry out all global pre-analyses required to infer cost in an interleaved way. Such resource analysis is parametric on the cost metrics one wants to measure (e.g., number of executed instructions, number of objects created, etc.). Besides, we present a novel form of cost summaries which allows us to incrementally reconstruct only those components of cost functions affected by the changes. Experimental results in the COSTA system show that the proposed incremental analysis provides significant performance gains, ranging from a speedup of 1.48 up to 5.13 times faster than non-incremental analysis.

@article{AlbertCPR13-tcs,
  author = {Elvira Albert and Jes\'us Correas and Germ\'{a}n Puebla and Guillermo Rom\'{a}n-D\'{i}ez},
  title = {A {M}ulti-{D}omain {I}ncremental {A}nalysis {E}ngine and its {A}pplication to {I}ncremental {R}esource {A}nalysis},
  journal = {Theoretical Computer Science},
  year = {2014},
  publisher = {Elsevier},
  note = {To appear},
  issn = {0304-3975}
}

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},
  doi = {http://dx.doi.org/10.1016/j.scico.2013.04.006},
  url = {http://dx.doi.org/10.1016/j.scico.2013.04.006},
  note = {To appear},
  issn = {0167-6423}
}

We present a novel static analysis to infer the peak cost of distributed systems. The different locations of a distributed system communicate and coordinate their actions by posting tasks among them. Thus, the amount of work that each location has to perform can greatly vary along the execution depending on: (1) the amount of tasks posted to its queue, (2) their respective costs, and (3) the fact that they may be posted in parallel and thus be pending to execute simultaneously. The peak cost of a distributed location refers to the maximum cost that it needs to carry out along its execution. Inferring the peak cost is challenging because it increases and decreases along the execution, unlike the standard notion of total cost which is cumulative. Our key contribution is the novel notion of quantified queue configuration which captures the worst-case cost of the tasks that may be simultaneously pending to execute at each location along the execution. Our analysis framework is developed for a generic notion of cost that can be instantiated to infer the peak cost in terms of number of steps, the amount of memory allocated, the number of tasks, etc. A prototype implementation demonstrates the accuracy and feasibility of the proposed peak cost analysis.

@inproceedings{AlbertCR14,
  author = {Elvira Albert and
               Jes\'us Correas and 
               Guillermo Rom\'an-D\'iez},
  title = {{P}eak {C}ost {A}nalysis of {D}istributed {S}ystems},
  booktitle = {21st International Static Analysis Symposium (SAS'14)},
  publisher = {Springer},
  year = {2014},
  note = {To appear}
}

We present the main concepts, usage and implementation of SACO, a static analyzer for concurrent objects. Interestingly, SACO is able to infer both liveness (namely termination and resource boundedness) and safety properties (namely deadlock freeness) of programs based on concurrent objects. The system integrates auxiliary analyses such as points-to and may-happen-in-parallel, which are essential for increasing the accuracy of the aforementioned more complex properties. SACO provides accurate information about the dependencies which may introduce deadlocks, loops whose termination is not guaranteed, and upper bounds on the resource consumption of methods.

@inproceedings{AlbertAFGGMPR14,
  author = {Elvira Albert and
               Puri Arenas and 
               Antonio Flores-Montoya and 
               Samir Genaim and 
               Miguel G\'omez-Zamalloa and
               Enrique Martin-Martin and 
               Germ\'an Puebla and
               Guillermo Rom\'an-D\'iez},
  title = {{SACO}: {S}tatic {A}nalyzer for {C}oncurrent {O}bjects},
  booktitle = {Tools and Algorithms for the Construction and Analysis of
               Systems - 20th International Conference, TACAS 2014, Held
               as Part of the European Joint Conferences on Theory and
               Practice of Software, ETAPS 2014, Grenoble, France, April
               5-13, 2014. Proceedings},
  year = {2014},
  editor = {Erika {\'A}brah{\'a}m and
               Klaus Havelund},
  pages = {562-567},
  volume = {8413},
  series = {Lecture Notes in Computer Science},
  isbn = {978-3-642-54861-1},
  publisher = {Springer},
  doi = {http://dx.doi.org/10.1007/978-3-642-54862-8_46},
  url = {http://link.springer.com/chapter/10.1007%2F978-3-642-54862-8_46}
}

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 = jun,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7940},
  pages = {285-300},
  url = {http://dx.doi.org/10.1007/978-3-642-38613-8_20}
}

Program properties that are automatically inferred by static analysis tools are generally not considered to be completely trustworthy, unless the tool implementation or the results are formally verified. Here we focus on the formal verification of resource guarantees inferred by automatic cost analysis. Resource guarantees ensure that programs run within the indicated amount of resources which may refer to memory consumption, to number of instructions executed, etc. In previous work we studied formal verification of inferred resource guarantees that depend only on integer data. In realistic programs, however, resource consumption is often bounded by the size of heap-allocated data structures. Bounding their size requires to perform a number of structural heap analyses. The contributions of this paper are (i) to identify what exactly needs to be verified to guarantee sound analysis of heap manipulating programs, (ii) to provide a suitable extension of the program logic used for verification to handle structural heap properties in the context of resource guarantees, and (iii) to improve the underlying theorem prover so that proof obligations can be automatically discharged.

@inproceedings{AlbertBGHR12,
  author = {Elvira Albert and Richard Bubel and Samir Genaim and Reiner
                  H\"ahnle and Guillermo Rom\'an-D\'iez},
  title = {{V}erified {R}esource {G}uarantees for {H}eap {M}anipulating {P}rograms},
  booktitle = {Proceedings of the 15th International Conference on Fundamental Approaches to Software Engineering, FASE 2012, Tallinn, Estonia, March, 2012},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  year = {2012},
  volume = {7212},
  month = mar,
  pages = {130-145},
  isbn = {978-3-642-28871-5},
  url = {http://www.springerlink.com/content/a10153194828v8k1/}
}

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 = jan,
  pages = {25--34},
  isbn = {978-1-4503-1118-2},
  doi = {10.1145/2103746.2103754},
  url = {http://dl.acm.org/citation.cfm?doid=2103746.2103754}
}

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{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 = dec,
  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 = jan,
  pages = {73-76},
  ee = {http://doi.acm.org/10.1145/1929501.1929513}
}

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 = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
  volume = {258},
  year = {2009},
  pages = {109-121},
  doi = {10.1016/j.entcs.2009.12.008},
  month = sep
}

This paper studies conditional termination of loops that involve array accesses, including loops which traverse circularly arrays, loops which use as loop bound or as loop counter an array element, etc. This kind of loops are commonly used, and their termination can only be proven if array contents are tracked. We present a new termination analysis for sequential bytecode programs which performs three main steps: (1) it first statically infers whether the memory locations of arrays remain constant along the execution of the loop and also whether there are aliases to such locations; (2) based on the inferred information, we provide sufficient conditions which guarantee if array accesses can be transformed into local variables; (3) when the conditions cannot be proven, we generate conditional termination assertions which, if satisfied, termination is guaranteed.

@inproceedings{AlbertGR12,
  author = {Elvira Albert and Samir Genaim and Guillermo Rom{\'a}n-D\'{\i}ez},
  title = {{C}onditional {T}ermination of {L}oops over {A}rrays},
  booktitle = {Proceedings of the Bytecode 2012 workshop, the Seventh
                  Workshop on Bytecode Semantics, Verification,
                  Analysis and Transformation (Bytecode 2012)},
  year = {2012},
  month = mar
}

Program properties that are automatically inferred by static analysis tools are generally not considered to be completely trustworthy, unless the tool implementation or the results are formally verified. Here we focus on the formal verification of resource guarantees inferred by automatic cost analysis. Resource guarantees ensure that programs run within the indicated amount of resources which may refer to memory consumption, to number of instructions executed, etc. In previous work we studied formal verification of inferred resource guarantees that depend only on integer data. In realistic programs, however, resource consumption is often bounded by the size of heap-allocated data structures. Bounding their size requires to perform a number of structural heap analyses. The contributions of this paper are (i) to identify what exactly needs to be verified to guarantee sound analysis of heap manipulating programs, (ii) to provide a suitable extension of the program logic used for verification to handle structural heap properties in the context of resource guarantees, and (iii) to improve the underlying theorem prover so that proof obligations can be automatically discharged.

@inproceedings{AlbertBGHR11,
  author = {Elvira Albert and Richard Bubel and Samir Genaim and Reiner H\"ahnle and Guillermo Rom\'an-D\'iez},
  title = {{V}erified {R}esource {G}uarantees for {H}eap {M}anipulating {P}rograms},
  booktitle = {10th KeY Symposium 2011},
  year = {2011},
  month = aug
}

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.

@inproceedings{FmcoTutorial12,
  title = {{A}utomatic {I}nference of {B}ounds on {R}esource {C}onsumption},
  author = {Elvira Albert and Diego Esteban 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 = {Formal Methods for Components and Objects - 11th International
               Symposium, FMCO 2012, Bertinoro, Italy, September 24-28,
               2012, Revised Lectures},
  year = {2013},
  pages = {119-144},
  volume = {7866},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  doi = {http://dx.doi.org/10.1007/978-3-642-40615-7_4},
  url = {http://dx.doi.org/10.1007/978-3-642-40615-7_4}
}