The goal of quantitative resource analysis is to provide developers with quantitative information about the runtime behavior of software at development time. With this extra information, programmers have early feedback to improve the efficiency of their code even before profiling.
Formal quantitative resource analysis also provides a well-designed framework to mathematically prove resource usage claims on programs. These strong guarantees are of tremendous importance for safety-critical and real-time systems.
This work presents a new framework to interactively and automatically derive certified, and compositional worst-case resource bounds.
We present here our tool C4B in a simple web interface. This automated
analysis is the first tool to successfully combine amortized analysis
reasoning with negative integer variables and imperative features like
assignment or non-linear control flow (like
How to analyze a file?
If your input file contains only one function, the body of this function
will be analyzed. If multiple function definitions are available,
only the body of the function
start will be analyzed. The
main function you analyze cannot be recursive, to analyze a recursive
f, define it and call it from
You can use two metrics to analyze a file. Either the standard
back-edge metric that assigns a cost of 1 to every back edge in
the control-flow graph (including function returns). Or the
tick metric that assigns a cost n for calls
tick(n) of the builtin
To use the latter metric, include the
directive in your C code. For an example usage of this metric,
load the example
The prototype above is not yet feature complete for C. In particular:
returncan only return variables.
gotois not supported.
We wrote a formal proof of soundness for our quantitative logic in the Coq proof assistant. The files in the archive below define precisely the semantics of a resource aware version of C and the rules of a logic to derive sound bounds for programs in this language.
You can also download a technical report that explains the details of our framework. The Section 2 of this file is a long informal explanation of both the logic and the automatic analysis. It features many examples with detailed explanations of our system. The Appendix A shows many other examples and features a comparison of different tools on these examples.