Static Cost Analysis aims at estimating the amount of resources that an execution of a given program consumes. By resource we mean any quantitative measure such as number of issued instructions, memory space usage, visits to a program point, etc.

The classical approach to cost analysis is based on transforming a given program into a system of cost relations (recurrence relations) and solving them into closed-form upper bounds and lower bounds. It is known that for some programs, the classical approach infers bounds that are asymptotically less precise than the actual cost. It was assumed that this imprecision is merely due to the way cost relations are solved into upper and lower bounds. In this talk we show that this assumption is partially true, and identify the reason due to which cost relations cannot precisely model the cost of such programs.

To overcome this imprecision, we develop the notion of net-cost functions, that model the cost of terminating executions of a program procedure as a function of its inputs and outputs. We show a method to verify upper and lower bounds on the net-cost, using a Satisfiability modulo Tarski theory of real closed fields (real numbers). This method is extended to template-based synthesis of net-cost bounds, by using Quantifier Elimination modulo that same theory.