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

Arthur Charguéraud 1, 2 François Pottier 3
1 CAMUS - Compilation pour les Architectures MUlti-coeurS
Inria Nancy - Grand Est, ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Abstract : 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.
Document type :
Journal articles
Liste complète des métadonnées

Cited literature [57 references]  Display  Hide  Download

https://hal.inria.fr/hal-01652785
Contributor : Arthur Charguéraud <>
Submitted on : Thursday, November 30, 2017 - 4:43:43 PM
Last modification on : Monday, November 26, 2018 - 1:28:02 PM

File

credits_jar.pdf
Files produced by the author(s)

Identifiers

Citation

Arthur Charguéraud, François Pottier. Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. Journal of Automated Reasoning, Springer Verlag, 2017, ⟨10.1007/s10817-017-9431-7⟩. ⟨hal-01652785⟩

Share

Metrics

Record views

251

Files downloads

135