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

DOI10.1007/978-3-540-71316-6_13zbMath1187.68150OpenAlexW1607674807MaRDI QIDQ5756496

Rodrigo Ferreira, Zhong Shao, Xinyu Feng

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)

Related Items (9)

Certifying low-level programs with hardware interrupts and preemptive threads ⋮ Compositional System Security with Interface-Confined Adversaries ⋮ Formal verification of concurrent programs with Read-write locks ⋮ Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ 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

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