Verifying a concurrent garbage collector with a rely-guarantee methodology (Q2319995): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-018-9489-x
+Normal rank
@@ Property / OpenAlex ID @@
+W2899108093
@@ Property / OpenAlex ID: W2899108093 / rank @@
+Normal rank
@@ Property / cites work @@
+A semantics for concurrent separation logic
@@ Property / cites work: A semantics for concurrent separation logic / rank @@
+Normal rank
@@ Property / cites work @@
+The reflective Milawa theorem prover is sound (down to the machine code that runs it)
+Normal rank
@@ Property / cites work @@
+Plan B
@@ Property / cites work: Plan B / rank @@
+Normal rank
@@ Property / cites work @@
+On-the-fly garbage collection
@@ Property / cites work: On-the-fly garbage collection / rank @@
+Normal rank
@@ Property / cites work @@
+A calculus of atomic actions
@@ Property / cites work: A calculus of atomic actions / rank @@
+Normal rank
@@ Property / cites work @@
+Automated verification of practical garbage collectors
+Normal rank
@@ Property / cites work @@
+Tentative steps toward a development method for interfering programs
+Normal rank
@@ Property / cites work @@
+A rely-guarantee-based simulation for verifying concurrent program transformations
+Normal rank
@@ Property / cites work @@
+A certified framework for compiling and executing garbage-collected languages
+Normal rank
@@ Property / cites work @@
+An axiomatic proof technique for parallel programs
+Normal rank
@@ Property / cites work @@
+Formal Derivation of Concurrent Garbage Collectors
+Normal rank
@@ Property / cites work @@
+Q4417904
@@ Property / cites work: Q4417904 / rank @@
+Normal rank
@@ Property / cites work @@
+A verified generational garbage collector for CakeML
+Normal rank
@@ Property / cites work @@
+CompCertTSO
@@ Property / cites work: CompCertTSO / rank @@
+Normal rank
@@ Property / cites work @@
+Local reasoning about a copying garbage collector
@@ Property / cites work: Local reasoning about a copying garbage collector / rank @@
+Normal rank
@@ Property / cites work @@
+Concurrent Separation Logic and Operational Semantics
+Normal rank
@@ Property / cites work @@
+A Marriage of Rely/Guarantee and Separation Logic
@@ Property / cites work: A Marriage of Rely/Guarantee and Separation Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying a concurrent garbage collector using a rely-guarantee methodology
+Normal rank