Verifying Visibility-Based Weak Consistency
From MaRDI portal
Publication:5041095
DOI10.1007/978-3-030-44914-8_11MaRDI QIDQ5041095
Constantin Enea, Michael Emmi, Dejan Jovanović, Siddharth Krishna
Publication date: 13 October 2022
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1911.01508
68Q60: Specification and verification (program logics, model checking, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Uses Software
Cites Work
- The existence of refinement mappings
- On reducing linearizability to state reachability
- \textsc{Poling}: SMT aided linearizability proofs
- Forward and backward simulations. I. Untimed Systems
- Proving linearizability using forward simulations
- Automated Verification of Practical Garbage Collectors
- E-matching for Fun and Profit
- Quantitative relaxation of concurrent data structures
- Proving Linearizability Using Partial Orders
- Dafny: An Automatic Program Verifier for Functional Correctness
- On abstraction and compositionality for weak-memory linearisability
- Owicki-Gries Reasoning for Weak Memory Models
- Shape-Value Abstraction for Verifying Linearizability
- RGSep Action Inference
- Verifying properties of parallel programs
- Local linearizability for concurrent container-type data structures
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Aspect-oriented linearizability proofs
- CONCUR 2004 - Concurrency Theory
- An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
- Automated Deduction – CADE-20
- Replicated data types
- Comparison Under Abstraction for Verifying Linearizability
