Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation

Arthur Charguéraud 1, 2 François Pottier 3
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is non-trivial. We present a Coq formalization of this analysis. 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. Reasoning in Coq about imperative OCaml code relies on the CFML tool, which is based on characteristic formulae and Separation Logic, 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.
Type de document :
Communication dans un congrès
6th International Conference on Interactive Theorem Proving (ITP), Aug 2015, Nanjing, China. 2015, 〈10.1007/978-3-319-22102-1_9〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01245872
Contributeur : Arthur Charguéraud <>
Soumis le : jeudi 17 décembre 2015 - 17:26:55
Dernière modification le : vendredi 17 février 2017 - 16:10:32
Document(s) archivé(s) le : samedi 29 avril 2017 - 19:14:09

Fichier

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

Identifiants

Citation

Arthur Charguéraud, François Pottier. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. 6th International Conference on Interactive Theorem Proving (ITP), Aug 2015, Nanjing, China. 2015, 〈10.1007/978-3-319-22102-1_9〉. 〈hal-01245872〉

Partager

Métriques

Consultations de
la notice

238

Téléchargements du document

55