On reducing linearizability to state reachability

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

Mathematics Subject Classification ID

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