The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Automated Resource Analysis with Coq Proof Objects

Last modified: Sat Jul 29 17:05:20 2017 GMT.

CAV Artifact Evaluation

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

  • Copyright © 1996-2024 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon