A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification

Abstract

We present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. We build on top of Separation Logic with Time Credits, embedded in an interactive proof assistant. We formalize the O notation, which is key to enabling modular specifications and proofs. We cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. We propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.

Paper

Armaël Guéneau, Arthur Charguéraud, and François Pottier
ESOP: European Symposium on Programming, April 2018