On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning

DOI10.1007/978-3-540-71316-6_13MaRDI QIDQ5756496zbMATH OpenOpenAlexFDO

Authors Xinyu Feng, Rodrigo Ferreira, Zhong Shao

Publication date 4 September 2007

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71316-6_13

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Revisiting concurrent separation logic
• Concurrent separation logic and operational semantics
• Syntactic control of interference and concurrent separation logic
• On the relation between concurrent separation logic and concurrent Kleene algebra
• An asynchronous soundness theorem for concurrent separation logic

Cited in

(14)

• Verification of asynchronous systems with an unspecified component
• Decision problems in a logic for reasoning about reconfigurable distributed systems
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
• scientific article; zbMATH DE number 6215728 (Why is no real title available?)
• Compositional system security with interface-confined adversaries
• Formal verification of concurrent programs with Read-write locks
• A Marriage of Rely/Guarantee and Separation Logic
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Specifying and reasoning about shared-variable concurrency
• Extending rely-guarantee thinking to handle real-time scheduling
• A compositional theory of linearizability
• Certifying low-level programs with hardware interrupts and preemptive threads
• Balancing expressiveness in formal approaches to concurrency

This page was built for publication: On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning

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