A semantics for concurrent separation logic

DOI10.1016/J.TCS.2006.12.034zbMath1111.68021OpenAlexW2125398300WikidataQ29396804 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

semanticsconcurrencylogicrace conditionpointers

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Related Items (46)

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

Cites Work

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

This page was built for publication: A semantics for concurrent separation logic