Authors

Quentin Carbonneaux
Jan Hoffmann
Thomas Reps
Zhong Shao

Abstract

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.

Published

In Proc. 29th International Conference on Computer Aided Verification (CAV 2017), Heidelberg, Germany, Part II, pages 64-85, July 2017.

Conference Paper PDF