Verifying Visibility-Based Weak Consistency (Q5041095): Difference between revisions

@@ Property / cites work @@
+The existence of refinement mappings
@@ Property / cites work: The existence of refinement mappings / rank @@
+Normal rank
@@ Property / cites work @@
+An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
+Normal rank
@@ Property / cites work @@
+Comparison Under Abstraction for Verifying Linearizability
+Normal rank
@@ Property / cites work @@
+On reducing linearizability to state reachability
@@ Property / cites work: On reducing linearizability to state reachability / rank @@
+Normal rank
@@ Property / cites work @@
+Proving linearizability using forward simulations
@@ Property / cites work: Proving linearizability using forward simulations / rank @@
+Normal rank
@@ Property / cites work @@
+Replicated data types
@@ Property / cites work: Replicated data types / rank @@
+Normal rank
@@ Property / cites work @@
+Aspect-oriented linearizability proofs
@@ Property / cites work: Aspect-oriented linearizability proofs / rank @@
+Normal rank
@@ Property / cites work @@
+On abstraction and compositionality for weak-memory linearisability
+Normal rank
@@ Property / cites work @@
+Local linearizability for concurrent container-type data structures
+Normal rank
@@ Property / cites work @@
+Automated Verification of Practical Garbage Collectors
+Normal rank
@@ Property / cites work @@
+Quantitative relaxation of concurrent data structures
+Normal rank
@@ Property / cites work @@
+Iris from the ground up: A modular foundation for higher-order concurrent separation logic
+Normal rank
@@ Property / cites work @@
+Proving Linearizability Using Partial Orders
@@ Property / cites work: Proving Linearizability Using Partial Orders / rank @@
+Normal rank
@@ Property / cites work @@
+Owicki-Gries Reasoning for Weak Memory Models
@@ Property / cites work: Owicki-Gries Reasoning for Weak Memory Models / rank @@
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+Forward and backward simulations. I. Untimed Systems
+Normal rank
@@ Property / cites work @@
+E-matching for Fun and Profit
@@ Property / cites work: E-matching for Fun and Profit / rank @@
+Normal rank
@@ Property / cites work @@
+CONCUR 2004 - Concurrency Theory
@@ Property / cites work: CONCUR 2004 - Concurrency Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying properties of parallel programs
@@ Property / cites work: Verifying properties of parallel programs / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Shape-Value Abstraction for Verifying Linearizability
+Normal rank
@@ Property / cites work @@
+RGSep Action Inference
@@ Property / cites work: RGSep Action Inference / rank @@
+Normal rank
@@ Property / cites work @@
+\textsc{Poling}: SMT aided linearizability proofs
@@ Property / cites work: \textsc{Poling}: SMT aided linearizability proofs / rank @@
+Normal rank