Local Reasoning about Data Update

Venue

Electronic Notes in Theoretical Computer Science 2007

Publication date

Apr 2007

Identifiers

DOI: doi:10.1016/j.entcs.2007.02.006

Authors

Cristiano Calcagno
Philippa Gardner
Uri Zarfaty

Abstract

We present local Hoare reasoning about data update, using Context Logic for analysing structured data. We apply our reasoning to tree update, heap update which is analogous to local Hoare reasoning using Separation Logic, and term rewriting.

Source Materials

Authors' Preprint/Accepted Version
Published Version
Published Edition
BibTeX Citation