Upper Bounds of Resource Usage for Java Bytecode using COSTA and its Web Interface?

costa [2] is a research prototype which performs automatic program analysis, in the style of [9, 7, 8], and which is able to infer cost [4] and termination [1] 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 [5], 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 [3], 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 [6]. 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). In this presentation we will show the recently developed costa web interface. It allows users to try out the system on a set of representative examples, and also to upload their own bytecode programs such as class or jar files. As the behaviour of costa can be customized using a relatively large set of options, the web interface allows two different alternatives for choosing the values for such options