Shape-Value Abstraction for Verifying Linearizability
From MaRDI portal
Publication:3600484
DOI10.1007/978-3-540-93900-9_27zbMATH Open1206.68103OpenAlexW71333976MaRDI QIDQ3600484FDOQ3600484
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
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
- Title not available (Why is that?)
- Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
- Comparison Under Abstraction for Verifying Linearizability
- Parametrized invariance for infinite state processes
- 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)
