Thamsborg, Jacob and Birkedal, Lars and Yang, Hongseok - Two for the Price of One: Lifting Separation Logic Assertions

lmcs:997 - Logical Methods in Computer Science, September 21, 2012, Volume 8, Issue 3
Two for the Price of One: Lifting Separation Logic Assertions

Authors: Thamsborg, Jacob and Birkedal, Lars and Yang, Hongseok

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.


Source : oai:arXiv.org:1208.5895
DOI : 10.2168/LMCS-8(3:22)2012
Volume: Volume 8, Issue 3
Published on: September 21, 2012
Submitted on: July 6, 2011
Keywords: Computer Science - Programming Languages,F.3.1


Share

Consultation statistics

This page has been seen 64 times.
This article's PDF has been downloaded 10 times.