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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/hal-01926485
Contributor : François Pottier <>
Submitted on : Monday, November 19, 2018 - 11:45:45 AM
Last modification on : Thursday, June 27, 2019 - 1:56:03 PM
Long-term archiving on : Wednesday, February 20, 2019 - 2:08:09 PM

File

gueneau-chargeraud-pottier-eso...
Files produced by the author(s)

Identifiers

Citation

Armaël Guéneau, Arthur Charguéraud, François Pottier. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. ⟨10.1007/978-3-319-89884-1_19⟩. ⟨hal-01926485⟩

Share

Metrics

Record views

91

Files downloads

185