COSTA: COSt and Termination Analyzer for Java Bytecode

Welcome to COSTA's web interface!

In order to start using it straight away, please go to the Analyzer section and follow the instructions there provided.

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-analyses, 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.