A separation logic for a promising semantics

DOI10.1007/978-3-319-89884-1_13zbMATH Open1422.68037OpenAlexW2797152240MaRDI QIDQ2323985FDOQ2323985

Authors: Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis 

Publication date: 13 September 2019

Full work available at URL: https://doi.org/10.1007/978-3-319-89884-1_13

Recommendations

• CONCUR 2004 - Concurrency Theory
• A semantics for concurrent separation logic
• Program verification under weak memory consistency using separation logic
• A separation logic for fictional sequential consistency
• Concurrent separation logic and operational semantics

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)

Cited In (23)

• Title not available (Why is that?)
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• A separation logic for fictional sequential consistency
• CONCUR 2004 - Concurrency Theory
• The decidability of verification under PS 2.0
• Multimodal Separation Logic for Reasoning About Operational Semantics
• Weak updates and separation logic
• Reasoning about promises in weak memory models with event structures
• Mechanised operational reasoning for C11 programs with relaxed dependencies
• A syntactic approach to Maksimova's principle of variable separation for some substructural logics
• An undecidability result for separation logic with theory reasoning
• Separation Logic Semantics for Communicating Processes
• Title not available (Why is that?)
• Step-indexed Kripke model of separation logic for storable locks
• A Semantics for Propositions as Sessions
• Hybrid logics of separation axioms
• A fine-grained semantics for arrays and pointers under weak memory models
• Tractable Reasoning in a Fragment of Separation Logic
• Making Linearizability Compositional for Partially Ordered Executions
• Rely-guarantee reasoning for causally consistent shared memory
• Compositional reasoning for non-multicopy atomic architectures
• Separation logic with linearly compositional inductive predicates and set data constraints

This page was built for publication: A separation logic for a promising semantics

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