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

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