A Verified Imperative Implementation of B-Trees

Title:	A Verified Imperative Implementation of B-Trees
Author:	Niels Mündler (n /dot/ muendler /at/ tum /dot/ de)
Submission date:	2021-02-24
Abstract:	In this work, we use the interactive theorem prover Isabelle/HOL to verify an imperative implementation of the classical B-tree data structure invented by Bayer and McCreight [ACM 1970]. The implementation supports set membership, insertion and deletion queries with efficient binary search for intra-node navigation. This is accomplished by first specifying the structure abstractly in the functional modeling language HOL and proving functional correctness. Using manual refinement, we derive an imperative implementation in Imperative/HOL. We show the validity of this refinement using the separation logic utilities from the Isabelle Refinement Framework . The code can be exported to the programming languages SML, OCaml and Scala. We examine the runtime of all operations indirectly by reproducing results of the logarithmic relationship between height and the number of nodes. The results are discussed in greater detail in the corresponding Bachelor's Thesis.
Change history:	[2021-05-02]: Add implementation and proof of correctness of imperative deletion operations. Further add the option to export code to OCaml.
BibTeX:	@article{BTree-AFP, author = {Niels Mündler}, title = {A Verified Imperative Implementation of B-Trees}, journal = {Archive of Formal Proofs}, month = feb, year = 2021, note = {\url{https://isa-afp.org/entries/BTree.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Refine_Imperative_HOL
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry