some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 9 (2013)

   Volume 10 (2014)

   Volume 11 (2015)

   Volume 12 (2016)

   Volume 13 (2017)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 8, ISSUE 3, PAPER 22


Two for the Price of One: Lifting Separation Logic Assertions

©Jacob Thamsborg, IT University of Copenhagen
©Lars Birkedal, IT University of Copenhagen
©Hongseok Yang, University of Oxford

Abstract
Recently, data abstraction has been studied in the context of separation logic, with noticeable practical successes: the developed logics have enabled clean proofs of tricky challenging programs, such as subject-observer patterns, and they have become the basis of efficient verification tools for Java (jStar), C (VeriFast) and Hoare Type Theory (Ynot). In this paper, we give a new semantic analysis of such logic-based approaches using Reynolds's relational parametricity. The core of the analysis is our lifting theorems, which give a sound and complete condition for when a true implication between assertions in the standard interpretation entails that the same implication holds in a relational interpretation. Using these theorems, we provide an algorithm for identifying abstraction-respecting client-side proofs; the proofs ensure that clients cannot distinguish two appropriately-related module implementations.

Publication date: September 21, 2012

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-8(3:22)2012

Hit Counts: 3185

Creative Commons