Compositional Certified Resource Bounds

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 break and return).

C4B Online

find out the runtime complexity of C programs

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 function f, define it and call it from start.

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 tick function. To use the latter metric, include the #pragma tick directive in your C code. For an example usage of this metric, load the example t46.

The prototype above is not yet feature complete for C. In particular:

Techical Report and Proofs

check out our Coq proofs

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.

Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao at Yale University