Automated Resource Analysis with Coq Proof Objects
Q. Carbonneaux, J. Hoffmann, T. Reps, and Z. Shao
This paper addresses the problem of automatically performing
resource-bound analysis, which can help programmers understand
the performance characteristics of their programs.
We introduce a method for resource-bound inference that
(i) is compositional, (ii) produces machine-checkable
certificates of the resource bounds obtained,
and (iii) features a sound mechanism for user interaction if the inference fails.
The technique handles recursive procedures and has the ability to
exploit any known program invariants.
An experimental evaluation with an implementation in the tool Pastis
shows that the new analysis is competitive with state-of-the-art
resource-bound tools while also creating Coq certificates.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)