COSTA
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). The COSTA web interface allows users to try out the system on a set of representative examples, and also to upload their own bytecode programs. As the behaviour of COSTA can be customized using a relatively large set of options, the web interface offers two different alternatives for choosing the values for such options. The first alternative, which we call automatic, allows the user to choose from a range of possibilities which differ in the analysis accuracy and overhead. All this, without requiring the user to understand the different options implemented in the system and their implications in analysis accuracy and overhead. The second alternative is called manual and it is meant for the expert user. There, the user has access to all of the analysis options available, allowing a fine-grained control over the behaviour of the analyzer. Some of these options include whether to analyze the Java standard libraries, to take exceptions into account, to perform a number of pre-a! nalyses, to write/read analysis results to file in order to reuse them in later analyses, etc. COSTA can analyze code for both Java SE and Java ME, in particular for the MIDP profile for mobile phones.
Keywords for this software
References in zbMATH (referenced in 24 articles , 1 standard article )
Showing results 1 to 20 of 24.
Sorted by year (- Hamilton, G. W.: Distilling programs to prove termination (2020)
- Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo: Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs (2019)
- Hainry, Emmanuel; Péchoux, Romain: A type-based complexity analysis of object oriented programs (2018)
- Nishida, Naoki; Vidal, Germán: A framework for computing finite SLD trees (2015)
- Ben-Amram, Amir M.; Genaim, Samir: Ranking functions for linear-constraint loops (2014)
- Bubel, Richard; Montoya, Antonio Flores; Hähnle, Reiner: Analysis of executable software models (2014)
- Kersten, Rody; Parisen Toldin, Paolo; van Gastel, Bernard; van Eekelen, Marko: A Hoare logic for energy consumption analysis (2014)
- Hofmann, Martin; Rodriguez, Dulma: Automatic type inference for amortised heap-space analysis (2013)
- Albert, Elvira; Arenas, Puri; Genaim, Samir; Gómez-Zamalloa, Miguel; Puebla, Germán: Automatic inference of resource consumption bounds (2012)
- Ben-Amram, Amir M.; Genaim, Samir; Masud, Abu Naser: On the termination of integer loops (2012)
- Albert, Elvira; Arenas, Puri; Genaim, Samir; Puebla, Germán: Closed-form upper bounds in static cost analysis (2011)
- Broch Johnsen, Einar; Owe, Olaf; Schlatte, Rudolf; Tapia Tarifa, Silvia Lizeth: Validating timed models of deployment components with parametric concurrency (2011)
- Albert, Elvira; Arenas, Puri; Genaim, Samir; Herraiz, Israel; Puebla, German: Comparing cost functions in resource analysis (2010)
- Atkey, Robert: Amortised resource analysis with separation logic (2010)
- Albert, Elvira; Arenas, Puri; Genaim, Samir; Puebla, Germán; Zanardini, Damiano: Resource usage analysis and its application to resource certification (2009) ioport
- Hofmann, Martin; Rodriguez, Dulma: Efficient type-checking for amortised heap-space analysis (2009)
- Albert, Elvira; Arenas, Puri; Genaim, Samir; Puebla, German; Zanardini, Damiano: \textsccosta: design and implementation of a cost and termination analyzer for Java bytecode (2008) ioport
- Jamain, Adrien; Hand, David J.: Mining supervised classification performance studies: a meta-analytic investigation (2008)
- Avron, Arnon: A non-deterministic view on non-classical negations (2005)
- de Barros e Silva, Elves A.: Critical point theorems and applications to a semilinear elliptic problem (1996)