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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [34 references]  Display  Hide  Download

https://hal.inria.fr/hal-01417102
Contributor : François Pottier <>
Submitted on : Thursday, December 15, 2016 - 12:03:09 PM
Last modification on : Thursday, April 26, 2018 - 10:27:49 AM
Long-term archiving on : Thursday, March 16, 2017 - 1:29:17 PM

File

fpottier-hashtable.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-01417102⟩

Share

Metrics

Record views

191

Files downloads

179