A semantics for concurrent separation logic

DOI10.1016/j.tcs.2006.12.034zbMath1111.68021WikidataQ29396804 ScholiaQ29396804MaRDI QIDQ879367

Stephen Brookes

Publication date: 11 May 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.12.034

zbMATH Keywords

semantics; concurrency; logic; race condition; pointers

Mathematics Subject Classification ID

68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

03B70: Logic in computer science

68Q55: Semantics in the theory of computing

Related Items

Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Unnamed Item, Unnamed Item, Separation Logic Semantics for Communicating Processes, Higher-Order Separation Logic in Isabelle/HOLCF, Separation Logic Tutorial, Precision and the Conjunction Rule in Concurrent Separation Logic, A Resource Analysis of the π-calculus, Concurrent Separation Logic and Operational Semantics, Strict Linearizability and Abstract Atomicity, Automata-theoretic semantics of idealized Algol with passive expressions, Formal verification of concurrent programs with Read-write locks, Elucidating concurrent algorithms via layers of abstraction and reification, Blaming the client: on data refinement in the presence of pointers, Inter-process buffers in separation logic with rely-guarantee, Trace-based verification of imperative programs with I/O, An operational semantics for object-oriented concepts based on the class hierarchy, Fine-grained concurrency with separation logic, A calculus and logic of bunched resources and processes, A perspective on specifying and verifying concurrent modules, Designing a semantic model for a wide-spectrum language with concurrency, RGITL: a temporal logic framework for compositional reasoning about interleaved programs, Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations, Fifty years of Hoare's logic, Verifying a concurrent garbage collector with a rely-guarantee methodology, On the relation between concurrent separation logic and concurrent Kleene algebra, Revisiting concurrent separation logic, Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition, A Discrete Geometric Model of Concurrent Program Execution, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, Unnamed Item, Granularity and Concurrent Separation Logic, On Locality and the Exchange Law for Concurrent Processes, Compositional Reasoning, Completeness for a First-Order Abstract Separation Logic, A Formalisation of Smallfoot in HOL, Automated Theorem Proving for Assertions in Separation Logic with All Connectives

Cites Work

• Resources, concurrency, and local reasoning
• The temporal semantics of concurrent programs
• An axiomatic proof technique for parallel programs
• The essence of parallel Algol.
• A hard act to follow
• Full abstraction for a shared-variable parallel language
• Deadlock analysis in networks of communicating processes
• Local reasoning about a copying garbage collector
• Separation and information hiding
• Proofs of Networks of Processes
• Proving Liveness Properties of Concurrent Programs
• Monitors
• Verifying properties of parallel programs
• Parallel programming: An axiomatic approach
• The Logic of Bunched Implications
• Permission accounting in separation logic
• CONCUR 2004 - Concurrency Theory
• The structure of the “THE”-multiprogramming system
• A structured paging system
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item