Simplifying linearizability proofs with reduction and abstraction

DOI10.1007/978-3-642-12002-2_25MaRDI QIDQ3557084zbMATH OpenOpenAlexFDO

Authors Tayfun Elmas, Ali Sezgin, Omer Subasi, Serdar Tasiran, Shaz Qadeer

Publication date 27 April 2010

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-12002-2_25

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Aspect-oriented linearizability proofs
• Aspect-oriented linearizability proofs
• Proving linearizability using forward simulations
• Proving linearizability with temporal logic

Cited in

(9)

• Head linear reduction and pure proof net extraction
• Using refinement calculus techniques to prove linearizability
• On the complexity of linearizability
• A sound and complete proof technique for linearizability of concurrent data structures
• Shape-Value Abstraction for Verifying Linearizability
• Verifying linearizability with hindsight
• Comparison Under Abstraction for Verifying Linearizability
• Reasoning about TSO programs using reduction and abstraction
• A rely-guarantee-based simulation for cooperative semantics

This page was built for publication: Simplifying linearizability proofs with reduction and abstraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3557084)