Machine-Checked Correctness and Complexity of a Union-Find Implementation

Опубликовано 22 июня 2016, 19:12

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.