Fine-grained concurrency with separation logic

DOI10.1007/s10992-011-9195-1zbMath1252.03077OpenAlexW2109373243MaRDI QIDQ763473

Kamal Lodaya, Kalpesh Kapoor, 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

concurrent programsseparation logicprogram correctnessgarbage collectionresource logicsheap storage

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• A semantics for concurrent separation logic
• Resources, concurrency, and local reasoning
• Proving assertions about parallel programs
• A mechanically verified incremental garbage collector
• The semantics and proof theory of the logic of bunched implications
• Modular verification of a non-blocking stack
• Algorithms for on-the-fly garbage collection
• A Marriage of Rely/Guarantee and Separation Logic
• Monitors
• Verifying properties of parallel programs
• An exercise in proving parallel programs correct
• On-the-fly garbage collection
• The Logic of Bunched Implications
• BI as an assertion language for mutable data structures
• Permission accounting in separation logic
• An axiomatic basis for computer programming

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