A Verified Implementation of B+-Trees in Isabelle/HOL

August 18, 2022 · The Ethereal · 🏛 International Colloquium on Theoretical Aspects of Computing

🔮 THE ETHEREAL: The Ethereal
Pure theory — exists on a plane beyond code

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Niels Mündler, Tobias Nipkow arXiv ID 2208.09066 Category cs.LO: Logic in CS Cross-listed cs.DS Citations 0 Venue International Colloquium on Theoretical Aspects of Computing Last Checked 5 months ago
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.
Community shame:
Not yet rated
📄 View on arXiv 🌐 View on ar5iv 📑 PDF 🎉 Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

📜 Similar Papers

In the same crypt — Logic in CS