On reducing linearizability to state reachability
From MaRDI portal
Publication:1641012
DOI10.1016/j.ic.2018.02.014zbMath1395.68090arXiv1502.06882OpenAlexW2795782844MaRDI QIDQ1641012
Constantin Enea, Jad Hamza, Ahmed Bouajjani, Michael Emmi
Publication date: 14 June 2018
Published in: Information and Computation, Automata, Languages, and Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1502.06882
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
On the correctness problem for serializability, Verifying Visibility-Based Weak Consistency, On reducing linearizability to state reachability, Decidability and complexity for quiescent consistency and its variations, Decomposable Relaxation for Concurrent Data Structures, Decomposing data structure commutativity proofs with \(mn\)-differencing, Reachability in Parameterized Systems: All Flavors of Threshold Automata, Unnamed Item, Unnamed Item, Strict Linearizability and Abstract Atomicity
Cites Work
- Unnamed Item
- Abstraction for concurrent objects
- On reducing linearizability to state reachability
- Model-checking of correctness conditions for concurrent objects
- On the complexity of linearizability
- A Scalable, Correct Time-Stamped Stack
- Tractable Refinement Checking for Concurrent Objects
- Aspect-Oriented Linearizability Proofs
- Testing Shared Memories
- Verifying Concurrent Programs against Sequential Specifications
- An Integrated Specification and Verification Technique for Highly Concurrent Data Structures