A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures (Q2946743): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
ReferenceBot (talk | contribs)
Changed an Item
 
(8 intermediate revisions by 4 users not shown)
Property / author
 
Property / author: Heike Wehrheim / rank
Normal rank
 
Property / author
 
Property / author: Heike Wehrheim / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Line-up / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: KIV / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Z / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: RGITL / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2017559473 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The existence of refinement mappings / rank
 
Normal rank
Property / cites work
 
Property / cites work: Atomic snapshots of shared memory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Comparison Under Abstraction for Verifying Linearizability / rank
 
Normal rank
Property / cites work
 
Property / cites work: Atomic actions, and their refinements to isolated protocols / rank
 
Normal rank
Property / cites work
 
Property / cites work: Modular Safety Checking for Fine-Grained Concurrency / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2863833 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Data Refinement / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2724177 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formal Techniques for Networked and Distributed Systems – FORTE 2004 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Nonblocking Algorithms and Backward Simulation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Simplifying Linearizability Proofs with Reduction and Abstraction / rank
 
Normal rank
Property / cites work
 
Property / cites work: Abstraction for concurrent objects / rank
 
Normal rank
Property / cites work
 
Property / cites work: Reasoning about Optimistic Concurrency Using a Program Logic for History / rank
 
Normal rank
Property / cites work
 
Property / cites work: Trace-based derivation of a scalable lock-free stack algorithm / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3713577 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Aspect-Oriented Linearizability Proofs / rank
 
Normal rank
Property / cites work
 
Property / cites work: A criterion for atomicity revisited / rank
 
Normal rank
Property / cites work
 
Property / cites work: Universal extensions to simulate specifications / rank
 
Normal rank
Property / cites work
 
Property / cites work: Using refinement calculus techniques to prove linearizability / rank
 
Normal rank
Property / cites work
 
Property / cites work: Reduction / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3126969 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Forward and backward simulations. I. Untimed Systems / rank
 
Normal rank
Property / cites work
 
Property / cites work: Verifying linearizability with hindsight / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4524764 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Completeness of ASM Refinement / rank
 
Normal rank
Property / cites work
 
Property / cites work: Completeness of fair ASM refinement / rank
 
Normal rank
Property / cites work
 
Property / cites work: RGITL: a temporal logic framework for compositional reasoning about interleaved programs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Temporal Logic Verification of Lock-Freedom / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formal Verification of a Lock-Free Stack with Hazard Pointers / rank
 
Normal rank
Property / cites work
 
Property / cites work: A separation logic for refining concurrent objects / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4301167 / rank
 
Normal rank

Latest revision as of 18:31, 10 July 2024

scientific article
Language Label Description Also known as
English
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
scientific article

    Statements

    A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures (English)
    0 references
    0 references
    0 references
    0 references
    17 September 2015
    0 references
    KIV
    0 references
    Z
    0 references
    concurrent access
    0 references
    linearizability
    0 references
    nonatomic refinement
    0 references
    theorem proving
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references