Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1)
1

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

Dates and versions

hal-01417102 , version 1 (15-12-2016)

Identifiers

  • HAL Id : hal-01417102 , version 1

Cite

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⟩

Collections

INRIA INRIA2 ANR
99 View
202 Download

Share

Gmail Facebook Twitter LinkedIn More