Reasoning about B+ Trees with Operational Semantics and Separation Logic

Sexton, Alan P.; Thielecke, Hayo

doi:10.1016/j.entcs.2008.10.021

Reasoning about B+ Trees with Operational Semantics and Separation Logic (bibtex)

@article{SeTh08entcs,
  author =       {Alan P. Sexton and Hayo Thielecke},
  title =        {Reasoning about B+ Trees with Operational Semantics
                  and Separation Logic},
  journal =      {Electronic Notes in Theoretical Computer Science},
  volume =       218,
  year =         2008,
  pages =        {355--369},
  note =         {Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV)},
  issn =         {1571-0661},
  url =          {http://www.sciencedirect.com/science/article/B75H1-4TRCRM2-R/2/33ae59ac922be9bd180048acd65c04ea},
  doi =          {10.1016/j.entcs.2008.10.021},
  pdf =          {http://www.cs.bham.ac.uk/%7Eaps/research/papers/pdf/SeTh-ENTCS08-B+TreesOpSemanticsSeparationLogic.pdf},
}