A constructive approach for proving data structures' linearizability

DOI10.1007/978-3-662-48653-5_24MaRDI QIDQ1664147zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Data structures (68P05)

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

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)