Skip to Main content Skip to Navigation
Theses

Mechanized Verification of the Correctness and Asymptotic Complexity of Programs

Abstract : This dissertation is concerned with the question of formally verifying that the implementation of an algorithm is not only functionally correct (it always returns the right result), but also has the right asymptotic complexity (it reliably computes the result in the expected amount of time). In the algorithms literature, it is standard practice to characterize the performance of an algorithm by indicating its asymptotic time complexity, typically using Landau’s “big-O” notation. We first argue informally that asymptotic complexity bounds are equally useful as formal specifications, because they enable modular reasoning: a O bound abstracts over the concrete cost expression of a program, and therefore abstracts over the specifics of its implementation. We illustrate—with the help of small illustrative examples—a number of challenges with the use of the O notation, in particular in the multivariate case, that might be overlooked when reasoning informally. We put these considerations into practice by formalizing the O notation in the Coq proof assistant, and by extending an existing program verification framework, CFML, with support for a methodology enabling robust and modular proofs of asymptotic complexity bounds. We extend the existing framework of Separation Logic with Time Credits, which allows to reason at the same time about correctness and time complexity, and introduce negative time credits. Negative time credits increase the expressiveness of the logic, and enable onvenient reasoning principles as well as elegant specifications. At the level of specifications, we show how asymptotic complexity specifications using O can be integrated and composed within Separation Logic with Time Credits. Then, in order to establish such specifications, we develop a methodology that allows proofs of complexity in Separation Logic to be robust and carried out at a relatively high level of abstraction, by relying on two key elements: a mechanism for collecting and deferring constraints during the proof, and a mechanism for semi-automatically synthesizing cost expressions without loss of generality. We demonstrate the usefulness and practicality of our approach on a number of increasingly challenging case studies. These include algorithms whose complexity analysis is relatively simple (such as binary search, which is nonetheless out of the scope of many automated complexity analysis tools) and data structures (such as Okasaki’s binary random access lists). In our most challenging case study, we establish the correctness and amortized complexity of a state-of-the-art incremental cycle detection algorithm: our methodology scales up to highly non-trivial algorithms whose complexity analysis intimately depends on subtle functional invariants, and furthermore makes it possible to formally verify OCaml code which can then actually be used as part of real world programs.
Document type :
Theses
Complete list of metadata

Cited literature [138 references]  Display  Hide  Download

https://hal.inria.fr/tel-02437532
Contributor : Armaël Guéneau <>
Submitted on : Monday, January 13, 2020 - 6:58:46 PM
Last modification on : Monday, June 28, 2021 - 10:44:02 AM
Long-term archiving on: : Tuesday, April 14, 2020 - 6:49:27 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-02437532, version 1

Collections

INRIA | CDF | PSL

Citation

Armaël Guéneau. Mechanized Verification of the Correctness and Asymptotic Complexity of Programs. Programming Languages [cs.PL]. Université de Paris, 2019. English. ⟨tel-02437532⟩

Share

Metrics

Record views

168

Files downloads

595