@inproceedings{8db6a94599194ffb8dc2271fadbbd6cd,
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.",
keywords = "Refinement, Separation logic, Verification",
author = "Niels M{\"u}ndler and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022 ; Conference date: 27-09-2022 Through 29-09-2022",
year = "2022",
doi = "10.1007/978-3-031-17715-6_21",
language = "English",
isbn = "9783031177149",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "324--341",
editor = "Helmut Seidl and Zhiming Liu and Pasareanu, {Corina S.}",
booktitle = "Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings",
}