Resource Analysis in the COSTA System

Having information about the execution cost of programs, i.e., the amount of resources that the execution will require, is useful for many different purposes, including program optimization, verification and certification. Reasoning about execution cost is difficult and error-prone. Therefore, it is widely recognized that cost analysis, sometimes also referred to as resource analysis or automatic complexity analysis, is quite important. COSTA3 is a state-of-the-art cost and termination analyzer which automates this task. The system is able to infer upper and lower bounds on the resource consumption of a large class of programs. Given a program P, the analysis results allow bounding the cost of executing P on any input data x without having to actually run P (x). The first successful proposal for automatically computing the complexity of programs was the seminal work of Wegbreit [33]. Since then, a number of cost analysis frameworks have been proposed, mostly in the context of declar