The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Compositional Certified Resource Bounds

Last modified: Sat Apr 2 18:32:34 2016 GMT.

PLDI Artifact Evaluation

Authors

Quentin Carbonneaux
Jan Hoffmann
Zhong Shao

Abstract

This paper presents a new approach for automatically deriving worst-case resource bounds for C programs. The described technique combines ideas from amortized analysis and abstract interpretation in a unified framework to address four challenges for state-of-the-art techniques: compositionality, user interaction, generation of proof certificates, and scalability.

Compositionality is achieved by incorporating the potential method of amortized analysis. It enables the derivation of global whole-program bounds with local derivation rules by naturally tracking size changes of variables in sequenced loops and function calls. The resource consumption of functions is described abstractly and a function call can be analyzed without access to the function body. User interaction is supported with a new mechanism that clearly separates qualitative and quantitative verification. A user can guide the analysis to derive complex non-linear bounds by using auxiliary variables and assertions. The assertions are separately proved using established qualitative techniques such as abstract interpretation or Hoare logic. Proof certificates are automatically generated from the local derivation rules. A soundness proof of the derivation system with respect to a formal cost semantics guarantees the validity of the certificates. Scalability is attained by an efficient reduction of bound inference to a linear optimization problem that can be solved by off-the-shelf LP solvers.

The analysis framework is implemented in the publicly-available tool C4B. An experimental evaluation demonstrates the advantages of the new technique with a comparison of C4B with existing tools on challenging micro benchmarks and the analysis of more than 2900 lines of C code from the cBench benchmark suite.

Published

In Proc. 2015 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), Portland, OR, pages 467-478, June 2015.
  • Conference Paper PDF
  • C4B project web site
  • Extended Technical Report [PDF]

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