A constructive approach for proving data structures' linearizability

DOI10.1007/978-3-662-48653-5_24zbMATH Open1394.68098OpenAlexW2293623126MaRDI QIDQ1664147FDOQ1664147

Authors: Kfir Lev-Ari, Gregory Chockler, Idit Keidar 

Publication date: 24 August 2018

Full work available at URL: https://doi.org/10.1007/978-3-662-48653-5_24

Recommendations

• A sound and complete proof technique for linearizability of concurrent data structures
• Proving linearizability using partial orders
• Comparison Under Abstraction for Verifying Linearizability
• Order out of chaos: proving linearizability using local views
• Proving linearizability using forward simulations

Mathematics Subject Classification ID

Data structures (68P05)

Cited In (5)

• PROVING PRODUCTIVITY IN INFINITE DATA STRUCTURES
• Decomposing data structure commutativity proofs with \(mn\)-differencing
• Verification of mutable linear data structures and iterator-based algorithms in Dafny
• Order out of chaos: proving linearizability using local views
• Proving linearizability using partial orders

This page was built for publication: A constructive approach for proving data structures' linearizability

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