A Verified Implementation of B+-Trees in Isabelle/HOL
Niels M\"undler, Tobias Nipkow
TL;DR
This paper presents a formal verification of an imperative B+-tree implementation in Isabelle/HOL, ensuring correctness for membership, insertion, and range queries through a two-step refinement process from abstract to efficient code.
Contribution
It introduces a verified, executable B+-tree implementation in Isabelle/HOL, bridging abstract specifications and efficient imperative code.
Findings
Verified correctness of B+-tree operations in Isabelle/HOL
Refined from abstract set interface to efficient imperative implementation
Supports membership, insertion, and range queries efficiently
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Natural Language Processing Techniques · Advanced Database Systems and Queries