Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation

Abstract : Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is non-trivial. We present a Coq formalization of this analysis. Moreover, we implement Union-Find as an OCaml library and formally endow it with a modular specification that offers a full functional correctness guarantee as well as an amortized complexity bound. Reasoning in Coq about imperative OCaml code relies on the CFML tool, which is based on characteristic formulae and Separation Logic, and which we extend with time credits. Although it was known in principle that amortized analysis can be explained in terms of time credits and that time credits can be viewed as resources in Separation Logic, we believe our work is the first practical demonstration of this approach.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-01245872
Contributor : Arthur Charguéraud <>
Submitted on : Thursday, December 17, 2015 - 5:26:55 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Saturday, April 29, 2017 - 7:14:09 PM

File

credits_itp15.pdf
Files produced by the author(s)

Identifiers

Citation

Arthur Charguéraud, François Pottier. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. 6th International Conference on Interactive Theorem Proving (ITP), Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_9⟩. ⟨hal-01245872⟩

Share

Metrics

Record views

423

Files downloads

171