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

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