A separation logic for refining concurrent objects

DOI10.1145/1926385.1926415MaRDI QIDQ5408547zbMATH OpenOpenAlexWikidataFDO

Authors Aaron Turon, Mitchell Wand

Publication date 10 April 2014

Published in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.296.8498

zbMATH Keywords

atomicityconcurrent programmingformal verificationrefinementrely-guaranteeshared-memory concurrency

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Separation logic and concurrency
• Fine-grained concurrency with separation logic
• Modular reasoning about separation of concurrent data structures
• Granularity and concurrent separation logic
• A semantics for concurrent separation logic

Cited in

(12)

• Logical relations for fine-grained concurrency
• A sound and complete proof technique for linearizability of concurrent data structures
• Barriers in Concurrent Separation Logic
• Formal verification of concurrent programs with Read-write locks
• scientific article; zbMATH DE number 1304382 (Why is no real title available?)
• scientific article; zbMATH DE number 1546500 (Why is no real title available?)
• Unifying Concurrent Objects and Distributed Tasks
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• CONCUR 2004 - Concurrency Theory
• Modular reasoning about separation of concurrent data structures
• Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics
• Fine-grained concurrency with separation logic

This page was built for publication: A separation logic for refining concurrent objects

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