Inter-process buffers in separation logic with rely-guarantee
type: Item
instance of: scholarly article
title: Inter-process buffers in separation logic with rely-guarantee
zbMATH Open document ID: 1214.68131
author: Richard Bornat
author: Hasan Amjad
published in: Formal Aspects of Computing
publication date: 2010-12-17T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 5827628
zbMATH Keywords: separation logic
zbMATH Keywords: rely-guarantee
zbMATH Keywords: concurrency
describes a project that uses: SPARK
MaRDI profile type: Publication
full work available at URL: s00165-009-0141-8
OpenAlex ID: W2142118968
cites work: Towards Automatic Stability Analysis for Rely-Guarantee Proofs
cites work: Permission accounting in separation logic
cites work: Variables as resource in separation logic
cites work: Q2721096
cites work: A semantics for concurrent separation logic
cites work: Q5674963
cites work: Q5621092
cites work: Randomized wait-free concurrent objects (extended abstract)
cites work: An axiomatic basis for computer programming
cites work: Q4808839
cites work: Q4040791
cites work: Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
cites work: Proving pointer programs in higher-order logic
cites work: Verifying properties of parallel programs
cites work: Resources, concurrency, and local reasoning
cites work: The Logic of Bunched Implications
cites work: Q4783297
cites work: Modular verification of a non-blocking stack
cites work: Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
cites work: Modular Safety Checking for Fine-Grained Concurrency
cites work: A Marriage of Rely/Guarantee and Separation Logic
Wikidata QID: Q130880073
DOI: 10.1007/S00165-009-0141-8
description: scientific article; zbMATH DE number 5827628