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.
CITATION STYLE
Guéneau, A., Charguéraud, A., & Pottier, F. (2018). A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10801 LNCS, pp. 533–560). Springer Verlag. https://doi.org/10.1007/978-3-319-89884-1_19
Mendeley helps you to discover research relevant for your work.