Shape-Value Abstraction for Verifying Linearizability

DOI10.1007/978-3-540-93900-9_27MaRDI QIDQ3600484zbMATH OpenOpenAlexFDO

Authors Viktor Vafeiadis

Publication date 10 February 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-93900-9_27

Mathematics Subject Classification ID

Data structures (68P05)

Recommendations

• Comparison Under Abstraction for Verifying Linearizability
• Towards Abstraction-Based Verification of Shape Calculus
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• Simplifying linearizability proofs with reduction and abstraction
• Programming Languages and Systems
• Proving Linearizability Via Non-atomic Refinement
• Modular verification of concurrency-aware linearizability

Cited in

(15)

• Heap Decomposition for Concurrent Shape Analysis
• Towards Abstraction-Based Verification of Shape Calculus
• Proving linearizability with temporal logic
• Verifying visibility-based weak consistency
• Verifying concurrent graph algorithms
• Thread Quantification for Concurrent Shape Analysis
• Order out of chaos: proving linearizability using local views
• Abstraction for concurrent objects
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Parametrized invariance for infinite state processes
• Comparison Under Abstraction for Verifying Linearizability
• Verifying linearizability with hindsight
• Intermediate value linearizability: a quantitative correctness criterion

This page was built for publication: Shape-Value Abstraction for Verifying Linearizability

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