Machine-Checked Correctness and Complexity of a Union-Find Implementation
354 views · Published 13 June 2016 · 53:40 · Indexed 8 November 2026
Channel: Microsoft Research · 2016 · Science & Technology
Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is non-trivial. Using Coq and the CFML tool, Arthur Chargu'raud and I have verified the correctness and amortized complexity of an OCaml implementation of Union-Find. In this talk, I will give an overview of our approach, which uses higher-order separation logic extended with time credits. This approach allows us to state (and establish) a single specification that covers correctness and complexity at the same time.
