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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2017, 〈10.1007/s10817-017-9431-7〉
Liste complète des métadonnées

Littérature citée [57 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01652785
Contributeur : Arthur Charguéraud <>
Soumis le : jeudi 30 novembre 2017 - 16:43:43
Dernière modification le : samedi 20 octobre 2018 - 01:17:27

Fichier

credits_jar.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

214

Téléchargements de fichiers

64