Two for the price of one: lifting separation logic assertions

DOI10.2168/LMCS-8(3:22)2012MaRDI QIDQ2914243zbMATH OpenFDO

Authors Jacob Thamsborg, Hongseok Yang, Lars Birkedal

Publication date 25 September 2012

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

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

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)

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.

Recommendations

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

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

Describes a project that uses

Uses Software

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

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)