Welcome to COSTABS's web interface!

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

COSTABS is a research prototype which performs automatic program analysis and which is able to infer cost and termination information about ABS programs (more information on ABS can be found here). The system receives as input an ABS 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 cost model. COSTABS provides several notions of resource: number of instructions, size of functional data, number of concurrent objects and number of spawned tasks.

When performing cost analysis, COSTABS 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, COSTABS includes a dedicated solver called PUBS. An interesting feature of COSTABS 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 COSTABS web interface allows users to try out the system on a set of representative examples, and also to upload their own programs.