Expressive modular fine-grained concurrency specification

DOI10.1145/1926385.1926417MaRDI QIDQ5408549zbMATH OpenOpenAlexFDO

Authors Bart Jacobs, Frank Piessens

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 https://lirias.kuleuven.be/handle/123456789/278074

zbMATH Keywords

separation logicfine-grained concurrency

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Data structures (68P05) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Modular Safety Checking for Fine-Grained Concurrency
• Modular reasoning about separation of concurrent data structures
• Specifying and verifying concurrent algorithms with histories and subjectivity
• Abstract specifications for concurrent maps
• An integrated specification and verification technique for highly concurrent data structures

Cited in

(12)

• Steps in modular specifications for concurrent modules (invited tutorial paper)
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Logical relations for fine-grained concurrency
• The essence of higher-order concurrent separation logic
• Modular Safety Checking for Fine-Grained Concurrency
• Concurrent separation logic and operational semantics
• A perspective on specifying and verifying concurrent modules
• Abstract specifications for concurrent maps
• Barriers in Concurrent Separation Logic
• Specifying and verifying concurrent algorithms with histories and subjectivity
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Sound Automation of Magic Wands

Describes a project that uses

Uses Software

• VeriFast
• VCC
• Coq

This page was built for publication: Expressive modular fine-grained concurrency specification

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