Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits

Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is nontrivial. We present a Coq formalization of this analysis, following Alstrup et al.'s recent proof (2014). 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. In order to reason in Coq about imperative OCaml code, we use the CFML tool, which implements Separation Logic for a subset of OCaml, 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. Finally, in order to explain the meta-theoretical foundations of our approach, we define a Separation Logic with time credits for an untyped call-by-value lambda-calculus, and formally verify its soundness.

Current stuff (2017):

• The revised paper, which has been published in the Journal of Automated Reasoning.
• A self-contained archive that contains TLC, CFML, and our proofs about Union-Find. OCaml and Coq 8.5 are required.
• Another self-contained archive that contains TLC and our Coq formalization of Separation Logic with Time Credits for an untyped call-by-value lambda-calculus. Coq 8.5 is required.

Older stuff (2015):

• The conference paper, presented at ITP 2015 by Arthur Charguéraud and François Pottier.
• The self-contained archive that accompanies the conference paper. This archive contains TLC, CFML, and the proofs about Union-Find. OCaml and Coq 8.5 are required.