Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic

Abstract : We describe the specification and proof of an (imperative, sequential) hash table implementation. The usual dictionary operations (insertion, lookup, and so on) are supported, as well as iteration via folds and iterators. The code is written in OCaml and verified using higher-order separation logic, embedded in Coq, via the CFML tool and library. This case study is part of a larger project that aims to build a verified OCaml library of basic data structures.
Type de document :
Communication dans un congrès
Certified Programs and Proofs, Jan 2017, Paris, France. Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017)
Liste complète des métadonnées


https://hal.inria.fr/hal-01417102
Contributeur : François Pottier <>
Soumis le : jeudi 15 décembre 2016 - 12:03:09
Dernière modification le : vendredi 16 décembre 2016 - 10:27:09
Document(s) archivé(s) le : jeudi 16 mars 2017 - 13:29:17

Fichier

fpottier-hashtable.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01417102, version 1

Collections

Citation

François Pottier. Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic. Certified Programs and Proofs, Jan 2017, Paris, France. Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017). <hal-01417102>

Partager

Métriques

Consultations de
la notice

66

Téléchargements du document

31