A separation logic for a promising semantics

DOI10.1007/978-3-319-89884-1_13zbMath1422.68037OpenAlexW2797152240MaRDI QIDQ2323985

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

Publication date: 13 September 2019

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

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Making Linearizability Compositional for Partially Ordered Executions ⋮ Reasoning about promises in weak memory models with event structures ⋮ A fine-grained semantics for arrays and pointers under weak memory models ⋮ The decidability of verification under PS 2.0

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