The following pages link to Mathematizing C++ concurrency (Q5408531):
Displaying 21 items.
- Linearizability on hardware weak memory models (Q782494) (← links)
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723) (← links)
- TSO-to-TSO linearizability is undecidable (Q1629746) (← links)
- A formal C memory model for separation logic (Q1694027) (← links)
- A denotational semantics for SPARC TSO (Q2130595) (← links)
- Thread-modular analysis of release-acquire concurrency (Q2145344) (← links)
- Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations (Q2256965) (← links)
- Aliasing Restrictions of C11 Formalized in Coq (Q2938039) (← links)
- Tackling Real-Life Relaxed Concurrency with FSL++ (Q2988652) (← links)
- Lem: A Lightweight Tool for Heavyweight Semantics (Q3088021) (← links)
- Owicki-Gries Reasoning for Weak Memory Models (Q3449485) (← links)
- (Q3614671) (← links)
- Modular Relaxed Dependencies in Weak Memory Concurrency (Q5041113) (← links)
- Unifying Operational Weak Memory Verification: An Axiomatic Approach (Q5056374) (← links)
- (Q5376661) (← links)
- Operational semantics of a weak memory model with channel synchronization (Q5915975) (← links)
- Making Linearizability Compositional for Partially Ordered Executions (Q6104493) (← links)
- Optimal stateless model checking for causal consistency (Q6535346) (← links)
- Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models (Q6535632) (← links)
- Compositional reasoning for non-multicopy atomic architectures (Q6610380) (← links)
- Mechanised operational reasoning for C11 programs with relaxed dependencies (Q6610382) (← links)
