There exists a litany of existing systems which can analyze the resource usage of an input program. These systems lie on a spectrum of expressiveness and automation. Inference-based systems can automatically generate an upper bound on the resource use of a program, at the cost of generating less precise analyses of resource usage. Meanwhile, verification-based systems are more expressive but lack automation; these systems require the programmer to provide a resource bound themselves, but can verify richer dependent resource bounds which contain conditional expressions and program variables as a result.

This article presents automated dependent resource analysis, a set of techniques for inferring dependent bounds on program resource consumption. Our approach aims to combine the best of both worlds, introducing new techniques to infer a richer set of resource bounds and break out of this spectrum. Our system takes as input a cost model for the program and automatically infers a fine-grained upper bound on resource usage, a bound which can reference program variables and include conditional expressions. Additionally, our prototype implementation of our system can already infer the resource use of examples which were not inferrable by previous resource inference systems.