Using refinement calculus techniques to prove linearizability
DOI10.1007/S00165-012-0250-7zbMATH Open1259.68128OpenAlexW2048605787MaRDI QIDQ1941870FDOQ1941870
Authors: Bengt Jonsson 
Publication date: 22 March 2013
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-012-0250-7
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- Reduction
- Stepwise refinement of parallel algorithms
- A calculus of refinements for program derivations
- A theorem on atomicity in distributed algorithms
- Simplifying linearizability proofs with reduction and abstraction
- Reasoning about nonblocking concurrency
Cited In (8)
- Strict linearizability and abstract atomicity
- Compositional verification of termination-preserving refinement of concurrent programs
- Linearly-Used Continuations in the Enriched Effect Calculus
- Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
- A sound and complete proof technique for linearizability of concurrent data structures
- Proving Linearizability Via Non-atomic Refinement
- Intermediate value linearizability: a quantitative correctness criterion
- Relating trace refinement and linearizability
Uses Software
This page was built for publication: Using refinement calculus techniques to prove linearizability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1941870)
