Automated Resource Analysis with Coq Proof Objects
Last modified: Sat Jul 29 17:05:20 2017 GMT.
AbstractThis 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.
PublishedIn Proc. 29th International Conference on Computer Aided Verification (CAV 2017), Heidelberg, Germany, Part II, pages 64-85, July 2017.
Copyright © 1996-2017 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science