An Example of Local Reasoning in BI Pointer Logic: the Schorr−Waite Graph Marking Algorithm - Yang, H (Proceedings of the 1st Workshop on Semantics‚ Program Analysis‚ and Computing Environments for Memory Management, 2001)