Paper Info
Title
A Verified Implementation of B+-Trees in Isabelle/HOL
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.
Year
DOI
Venue
2022
10.1007/978-3-031-17715-6_21
International Colloquium on Theoretical Aspects of Computing (ICTAC)
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
Niels Mündler100.34
Tobias Nipkow23056232.28