A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL

DOI10.1007/978-3-031-17715-6_21arXiv2208.09066OpenAlexW4312856680MaRDI QIDQ6109486

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

verificationrefinementseparation logic

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Refinement to imperative HOL
• Organization and maintenance of large ordered indexes
• Automatic Functional Correctness Proofs for Functional Search Trees
• Concrete Semantics
• Imperative Functional Programming with Isabelle/HOL
• Toward a verified relational database management system
• Reasoning about B+ Trees with Operational Semantics and Separation Logic