A Program Logic for C11 Memory Fences
From MaRDI portal
Publication:2796064
DOI10.1007/978-3-662-49122-5_20zbMath1475.68083OpenAlexW2294707073MaRDI QIDQ2796064
Publication date: 23 March 2016
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-662-49122-5_20
Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (7)
Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Thread-modular analysis of release-acquire concurrency ⋮ Making Linearizability Compositional for Partially Ordered Executions ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Reasoning about promises in weak memory models with event structures ⋮ Tackling Real-Life Relaxed Concurrency with FSL++
Uses Software
This page was built for publication: A Program Logic for C11 Memory Fences
