Using refinement calculus techniques to prove linearizability

DOI10.1007/S00165-012-0250-7MaRDI QIDQ1941870zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

formal verificationrefinement calculuslinearizabilitymulti-threading

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Proving Linearizability Via Non-atomic Refinement
• A sound and complete proof technique for linearizability of concurrent data structures
• Proving linearizability with temporal logic
• Simplifying linearizability proofs with reduction and abstraction
• Relating trace refinement and linearizability

Cites work

• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• A calculus of refinements for program derivations
• A theorem on atomicity in distributed algorithms
• Reasoning about nonblocking concurrency
• Reduction
• Simplifying linearizability proofs with reduction and abstraction
• Stepwise refinement of parallel algorithms
• Verification, Model Checking, and Abstract Interpretation

Cited in

(8)

• Strict linearizability and abstract atomicity
• Compositional verification of termination-preserving refinement of concurrent programs
• Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
• Linearly-Used Continuations in the Enriched Effect Calculus
• 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

Describes a project that uses

Uses Software

• UNITY

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)