Local Reasoning About Tree Update

Separation Logic and Context Logic have been used to reason locally about heap update and simple tree update. We study local reasoning based on Context Logic for a more realistic, local tree-update language which combines update commands with queries. This combination results in updates at multiple locations, which significantly affects the complexity of the reasoning.