Resource Aware ML (RaML) is a tool that automatically and statically computes resource-use bounds for OCaml programs...
The system automatically derives upper bounds on the worst-case resource use and lower bounds on the best-case resource use. Furthermore, it can determine if the resource use is constant for inputs of a given size. RaML supports higher-order, polymorphic programs with side effects and user-defined inductive types. The derived bounds are multivariate resource polynomials that are functions of different size parameters that depend on the standard OCaml types. Bound inference is fully automatic and reduced to a linear optimization problem that is passed to an off-the-shelf LP solver...
Since symbolic bound inference is an undecidable problem, RaML cannot automatically derive a bound for every program. Our goal is therefore to find bounds for most programs that appear in practice.