COSTA: A Cost and Termination Analyzer for Java Bytecode

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