Fine-grained concurrency with separation logic

DOI10.1007/S10992-011-9195-1MaRDI QIDQ763473zbMATH OpenOpenAlexFDO

Authors Kalpesh Kapoor, Kamal Lodaya, Uday S. Reddy

Publication date 9 March 2012

Published in Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL http://pure-oai.bham.ac.uk/ws/files/12780883/fine_grained.pdf

zbMATH Keywords

separation logicprogram correctnessgarbage collectionresource logicsconcurrent programsheap storage

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Separation logic and concurrency
• Granularity and concurrent separation logic
• A semantics for concurrent separation logic
• CONCUR 2004 - Concurrency Theory
• A separation logic for refining concurrent objects

Cites work

• scientific article; zbMATH DE number 108539 (Why is no real title available?)
• scientific article; zbMATH DE number 3483531 (Why is no real title available?)
• scientific article; zbMATH DE number 3541921 (Why is no real title available?)
• scientific article; zbMATH DE number 1759448 (Why is no real title available?)
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• A Marriage of Rely/Guarantee and Separation Logic
• A mechanically verified incremental garbage collector
• A semantics for concurrent separation logic
• Algorithms for on-the-fly garbage collection
• An axiomatic basis for computer programming
• An exercise in proving parallel programs correct
• BI as an assertion language for mutable data structures
• Concurrency verification. Introduction to compositional and noncompositional methods
• Linear logic
• Modular verification of a non-blocking stack
• Monitors
• On-the-fly garbage collection
• Permission accounting in separation logic
• Proving assertions about parallel programs
• Resources, concurrency, and local reasoning
• The Logic of Bunched Implications
• The semantics and proof theory of the logic of bunched implications
• Verifying properties of parallel programs

Cited in

(15)

• Logical relations for fine-grained concurrency
• Barriers in Concurrent Separation Logic
• Specifying and verifying concurrent algorithms with histories and subjectivity
• Permission-based separation logic for multithreaded Java programs
• Granularity and concurrent separation logic
• Logical reasoning for disjoint permissions
• Reasoning over permissions regions in concurrent separation logic
• Separation logic and concurrency
• Formal verification of concurrent programs with Read-write locks
• Communicating state transition systems for fine-grained concurrent resources
• Permission accounting in separation logic
• A separation logic for refining concurrent objects
• Local Reasoning for Storable Locks and Threads
• Reasoning about optimistic concurrency using a program logic for history
• Permission-based separation logic for message-passing concurrency

This page was built for publication: Fine-grained concurrency with separation logic

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