A verified implementation of B^+-trees in Isabelle/HOL

DOI10.1007/978-3-031-17715-6_21MaRDI QIDQ6109486zbMATH OpenOpenAlexFDO

Authors Niels Mündler, Tobias Nipkow

Publication date 28 July 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2208.09066

zbMATH Keywords

refinementseparation logicverification

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Abstract: In this paper we present the verification of an imperative implementation of the ubiquitous B+-tree data structure in the interactive theorem prover Isabelle/HOL. The implementation supports membership test, insertion and range queries with efficient binary search for intra-node navigation. The imperative implementation is verified in two steps: an abstract set interface is refined to an executable but inefficient purely functional implementation which is further refined to the efficient imperative implementation.

Cites work

• Automatic functional correctness proofs for functional search trees
• Concrete semantics. With Isabelle/HOL
• scientific article; zbMATH DE number 3653523 (Why is no real title available?)
• scientific article; zbMATH DE number 1552508 (Why is no real title available?)
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Imperative Functional Programming with Isabelle/HOL
• Organization and maintenance of large ordered indexes
• Reasoning about B+ trees with operational semantics and separation logic
• Refinement to imperative HOL
• Toward a verified relational database management system

This page was built for publication: A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6109486)