RAML

Resource Aware ML (RAML) is a tool that automatically and statically computes resource-use bounds for OCaml programs.

In principle, a resource can be any quantity that is of interest to the user. We currently implemented resource metrics for the number of evaluation steps in a high-level abstract machine, allocated heap cells, and user-defined ticks executed.

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.

People

RAML is developed by the following people.

News

October 2016
Our paper Towards Automatic Resource Bound Analysis for OCaml will appear at POPL 2017.
October 2016
RAML 1.3.1 has been released.
July 2016
RAML 1.3 has been released.
July 2016
Three new working papers are online.
February 2016
Chan Ngo has joined the RAML team.
November 2015
RAML 1.1 has been released.
October 2015
Ankush Das joined the RAML team.
September 2015
RAML 1.0 has been released.
September 2015
Jan started as Tenure-Track Assistant Professor in Carnegie Mellon's Computer Science Department.