Reasoning about B+ Trees with Operational Semantics and Separation Logic

DOI10.1016/j.entcs.2008.10.021zbMath1286.68106OpenAlexW2136132549MaRDI QIDQ5415648

Alan P. Sexton, Hayo Thielecke

Publication date: 13 May 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.10.021

zbMATH Keywords

invariantseparation logicdata structureabstract machinesB+ trees

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Data structures (68P05)

Related Items

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

Cites Work

• Unnamed Item
• Organization and maintenance of large ordered indexes
• BI as an assertion language for mutable data structures
• Frame rules from answer types for code pointers
• The Mechanical Evaluation of Expressions