Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2019

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

(1, 2) , (3, 4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
credits_jar.pdf (372.81 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01652785 , version 1 (30-11-2017)

Identifiers

Cite

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, 2019, 62 (3), pp.331--365. ⟨10.1007/s10817-017-9431-7⟩. ⟨hal-01652785⟩
264 View
432 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More