A perspective on specifying and verifying concurrent modules
type: Item
instance of: scholarly article
title: A perspective on specifying and verifying concurrent modules
zbMATH Open document ID: 1395.68187
author: Thomas Dinsdale-Young
author: Pedro da Rocha Pinto
author: Philippa Gardner
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2018-06-27T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 6895011
zbMATH Keywords: concurrency
zbMATH Keywords: specification
zbMATH Keywords: program verification
describes a project that uses: VCC
MaRDI profile type: Publication
full work available at URL: j.jlamp.2018.03.003
OpenAlex ID: W2796428443
cites work: Verifying properties of parallel programs
cites work: Resources, concurrency, and local reasoning
cites work: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
cites work: Communicating State Transition Systems for Fine-Grained Concurrent Resources
cites work: Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
cites work: Expressive modular fine-grained concurrency specification
cites work: An axiomatic basis for computer programming
cites work: BI as an assertion language for mutable data structures
cites work: A semantics for concurrent separation logic
cites work: The Logic of Bunched Implications
cites work: Local rely-guarantee reasoning
cites work: Deny-Guarantee Reasoning
cites work: Q4813391
cites work: Permission accounting in separation logic
cites work: Subjective auxiliary state for coarse-grained concurrency
cites work: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
cites work: Modular Reasoning about Separation of Concurrent Data Structures
cites work: Impredicative Concurrent Abstract Predicates
cites work: Abstraction for Concurrent Objects
cites work: Views
cites work: Separation logic and abstraction
cites work: Linearizability with Ownership Transfer
cites work: Modular Termination Verification for Non-blocking Concurrency
cites work: Caper
cites work: CoLoSL: Concurrent Local Subjective Logic
DOI: 10.1016/J.JLAMP.2018.03.003
description: scientific article; zbMATH DE number 6895011