Local Reasoning for Global Graph Properties (Q5041096): Difference between revisions

@@ Property / describes a project that uses @@
+VeriFast
@@ Property / describes a project that uses: VeriFast / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VACID-0
@@ Property / describes a project that uses: VACID-0 / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3023197541
@@ Property / OpenAlex ID: W3023197541 / rank @@
+Normal rank
@@ Property / cites work @@
+Verified Software Toolchain
@@ Property / cites work: Verified Software Toolchain / rank @@
+Normal rank
@@ Property / cites work @@
+FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
+Normal rank
@@ Property / cites work @@
+Bringing Order to the Separation Logic Jungle
@@ Property / cites work: Bringing Order to the Separation Logic Jungle / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
+Normal rank
@@ Property / cites work @@
+Q5875421
@@ Property / cites work: Q5875421 / rank @@
+Normal rank
@@ Property / cites work @@
+Compositional entailment checking for a fragment of separation logic
+Normal rank
@@ Property / cites work @@
+Q4436059
@@ Property / cites work: Q4436059 / rank @@
+Normal rank
@@ Property / cites work @@
+The ramifications of sharing in data structures
@@ Property / cites work: The ramifications of sharing in data structures / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Science Logic
@@ Property / cites work: Computer Science Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Iris from the ground up: A modular foundation for higher-order concurrent separation logic
+Normal rank
@@ Property / cites work @@
+Back to the future
@@ Property / cites work: Back to the future / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+Recursive proofs for inductive tree data-structures
+Normal rank
@@ Property / cites work @@
+Viper: A Verification Infrastructure for Permission-Based Reasoning
+Normal rank
@@ Property / cites work @@
+Q4783297
@@ Property / cites work: Q4783297 / rank @@
+Normal rank
@@ Property / cites work @@
+Separation logic and abstraction
@@ Property / cites work: Separation logic and abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Concurrent Graph Algorithms
@@ Property / cites work: Verifying Concurrent Graph Algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+CoLoSL: Concurrent Local Subjective Logic
@@ Property / cites work: CoLoSL: Concurrent Local Subjective Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Priority inheritance protocols: an approach to real-time synchronization
+Normal rank
@@ Property / cites work @@
+An Efficient Decision Procedure for Imperative Tree Data Structures
+Normal rank