A separation logic for a promising semantics

DOI10.1007/978-3-319-89884-1_13MaRDI QIDQ2323985zbMATH OpenOpenAlexFDO

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

Publication date 13 September 2019

Copyright license Creative Commons Attribution 4.0 International

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

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)

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

Cited in

(23)

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

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)