Modular reasoning about separation of concurrent data structures

DOI10.1007/978-3-642-37036-6_11MaRDI QIDQ5326285zbMATH OpenOpenAlexFDO

Authors Kasper Svendsen, Matthew J. Parkinson, Lars Birkedal

Publication date 5 August 2013

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-37036-6_11

Mathematics Subject Classification ID

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

Recommendations

• A separation logic for refining concurrent objects
• Abstract specifications for concurrent maps
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• Separation logic and concurrency
• A semantics for concurrent separation logic

Cited in

(23)

• A perspective on specifying and verifying concurrent modules
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Building a Modal Interface Theory for Concurrency and Data
• Logical relations for fine-grained concurrency
• The essence of higher-order concurrent separation logic
• Abstract specifications for concurrent maps
• Modular verification of a non-blocking stack
• Modular Schedulability Analysis of Concurrent Objects in Creol
• scientific article; zbMATH DE number 1508923 (Why is no real title available?)
• Local reasoning for global graph properties
• Expressing the behavior of three very different concurrent systems by using natural extensions of separation logic
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Reasoning about separation using abstraction and reification
• Structural lock correlation with ownership types
• A separation logic for refining concurrent objects
• Modular reasoning for deterministic parallelism
• Expressive modular fine-grained concurrency specification
• Impredicative concurrent abstract predicates
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• Practical abstractions for automated verification of message passing concurrency
• A logical approach to type soundness

This page was built for publication: Modular reasoning about separation of concurrent data structures

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