Two for the price of one: lifting separation logic assertions

DOI10.2168/LMCS-8(3:22)2012zbMATH Open1258.03032arXiv1208.5895MaRDI QIDQ2914243FDOQ2914243

Authors: Jacob Thamsborg, Hongseok Yang, Lars Birkedal 

Publication date: 25 September 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1208.5895

Recommendations

• Relational Parametricity and Separation Logic
• Relational Parametricity and Separation Logic
• Separation logic and abstraction
• Relational separation logic
• Algebraic separation logic

zbMATH Keywords

data abstractionseparation logicrelational interpretation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cited In (4)

• Relational Parametricity and Separation Logic
• Abstraction and subsumption in modular verification of C programs
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Relational Parametricity and Separation Logic

Uses Software

• SIMPLIFY
• ESC/Java
• VeriFast
• Boogie
• jStar
• Ynot

This page was built for publication: Two for the price of one: lifting separation logic assertions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914243)