Fine-grained concurrency with separation logic

DOI10.1007/s10992-011-9195-1zbMath1252.03077MaRDI 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 programs; separation logic; program correctness; garbage collection; resource logics; heap storage

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item