Comparison Under Abstraction for Verifying Linearizability

DOI10.1007/978-3-540-73368-3_49MaRDI QIDQ5429339zbMATH OpenOpenAlexFDO

Authors Daphna Amit, Noam Rinetzky, Mooly Sagiv, Eran Yahav, Thomas Reps

Publication date 29 November 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73368-3_49

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Shape-Value Abstraction for Verifying Linearizability
• Simplifying linearizability proofs with reduction and abstraction
• Programming Languages and Systems
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• Verifying linearizability with hindsight
• Proving Linearizability Via Non-atomic Refinement

Cited in

(15)

• A constructive approach for proving data structures' linearizability
• A relational shape abstract domain
• On the complexity of linearizability
• Concurrent correctness in vector space
• Comparing abstraction refinement algorithms
• A sound and complete proof technique for linearizability of concurrent data structures
• Liveness-Preserving Atomicity Abstraction
• Shape-Value Abstraction for Verifying Linearizability
• Abstraction for Concurrent Objects
• Model checking simulation rules for linearizability
• Parametrized invariance for infinite state processes
• Verifying visibility-based weak consistency
• Order out of chaos: proving linearizability using local views
• Proving linearizability with temporal logic
• Checking linearizability of encapsulated extended operations

This page was built for publication: Comparison Under Abstraction for Verifying Linearizability

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