Weak updates and separation logic

Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

Separation Logic (SL) provides a simple but powerful technique for reasoning about imperative programs that use shared data structures. Unfortunately, SL supports only "strong updates", in which mutation to a heap location is safe only if a unique reference is owned. This limits the applicability of SL when reasoning about the interaction between many high-level languages (e.g., ML, Java, C#) and low-level ones since these high-level languages do not support strong updates. Instead, they adopt the discipline of "weak updates", in which there is a global "heap type" to enforce the invariant of type-preserving heap updates. We present SL w, a logic that extends SL with reference types and elegantly reasons about the interaction between strong and weak updates. We also describe a semantic framework for reference types; this framework is used to prove the soundness of SL w.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings
Pages178-193
Number of pages16
DOIs
StatePublished - Dec 28 2009
Event7th Asian Symposium on Programming Languages and Systems, APLAS 2009 - Seoul, Korea, Republic of
Duration: Dec 14 2009Dec 16 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5904 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other7th Asian Symposium on Programming Languages and Systems, APLAS 2009
CountryKorea, Republic of
CitySeoul
Period12/14/0912/16/09

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Weak updates and separation logic'. Together they form a unique fingerprint.

Cite this