Automated Amortized Resource Analysis (AARA) is a technique to statically derive polynomial, worst-case cost bounds on functional programs. The bounds AARA derives are sound, i.e., they provably upper bound the cost of the program being analyzed over all inputs. AARA excels at deriving tight worst-case bounds on structurally recursive programs, but is unable to express bounds involving logarithms. This manifests in an inability to tightly bound programs involving logarithmic depth recursion schemes (e.g., mergesort, heap-sort, etc). Dually, data-driven cost analyses rely on running the program of interest on sufficiently many inputs to infer a function on its cost in terms of the input size. Such methods are able to derive tight cost bounds, but at the expense of soundness.

Resource decomposition is a hybrid resource analysis technique which supplements AARA with data-driven resource analysis to be able to derive tighter cost bounds on programs that cannot be analyzed tightly by AARA. Its philosophy is to employ data-driven analysis to bound the recursion depth of functions that AARA struggles to analyze. In this work, I improve upon and integrate resource decomposition as a largely automated process in RaML 2, a cost analysis tool for Standard ML programs. I empirically demonstrate how RaML 2 with resource decomposition is able to derive tight bounds on common functional programs containing logarithmic components in their ground truth bounds.