Using refinement calculus techniques to prove linearizability

DOI10.1007/S00165-012-0250-7zbMath1259.68128OpenAlexW2048605787MaRDI QIDQ1941870

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

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

Related Items (2)

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Strict Linearizability and Abstract Atomicity

Uses Software

• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theorem on atomicity in distributed algorithms
• Stepwise refinement of parallel algorithms
• A calculus of refinements for program derivations
• Simplifying Linearizability Proofs with Reduction and Abstraction
• Reduction
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Using refinement calculus techniques to prove linearizability