Local Reasoning about Data Update

DOI10.1016/j.entcs.2007.02.006zbMath1277.68064OpenAlexW2074457838MaRDI QIDQ2864149

Uri Zarfaty, Cristiano Calcagno, Philippa Gardner

Publication date: 6 December 2013

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.2007.02.006

zbMATH Keywords

context logicheap updatelocal Hoare reasoningtree update

Mathematics Subject Classification ID

Logic in computer science (03B70) Grammars and rewriting systems (68Q42) Data structures (68P05)

Related Items (1)

Footprints in Local Reasoning

Uses Software

• Smallfoot

Cites Work

• Elimination of spatial connectives in static spatial logics
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• The semantics and proof theory of the logic of bunched implications
• Context logic as modal logic
• Variance analyses from invariance analyses
• The Logic of Bunched Implications
• Anytime, anywhere
• BI as an assertion language for mutable data structures
• Context logic and tree update
• An axiomatic basis for computer programming
• Automata, Languages and Programming
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Local Reasoning about Data Update