A Machine-Checked Framework for Relational Separation Logic (Q3095237): 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 @@
+VeriFast
@@ Property / describes a project that uses: VeriFast / 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/978-3-642-24690-6_10
+Normal rank
@@ Property / OpenAlex ID @@
+W2121753233
@@ Property / OpenAlex ID: W2121753233 / rank @@
+Normal rank
@@ Property / cites work @@
+A logic for information flow in object-oriented programs
+Normal rank
@@ Property / cites work @@
+Separation Logic for Small-Step cminor
@@ Property / cites work: Separation Logic for Small-Step cminor / rank @@
+Normal rank
@@ Property / cites work @@
+Formal certification of code-based cryptographic proofs
+Normal rank
@@ Property / cites work @@
+Simple relational correctness proofs for static analyses and program transformations
+Normal rank
@@ Property / cites work @@
+Programming with angelic nondeterminism
@@ Property / cites work: Programming with angelic nondeterminism / rank @@
+Normal rank
@@ Property / cites work @@
+Q2721096
@@ Property / cites work: Q2721096 / rank @@
+Normal rank
@@ Property / cites work @@
+Lightweight Separation
@@ Property / cites work: Lightweight Separation / rank @@
+Normal rank
@@ Property / cites work @@
+Verification of the Schorr-Waite Algorithm – From Trees to Graphs
+Normal rank
@@ Property / cites work @@
+Proving that non-blocking algorithms don't block
@@ Property / cites work: Proving that non-blocking algorithms don't block / rank @@
+Normal rank
@@ Property / cites work @@
+BI as an assertion language for mutable data structures
+Normal rank
@@ Property / cites work @@
+Practical Tactics for Separation Logic
@@ Property / cites work: Practical Tactics for Separation Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Proving pointer programs in higher-order logic
@@ Property / cites work: Proving pointer programs in higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+Separation Logic Adapted for Proofs by Rewriting
@@ Property / cites work: Separation Logic Adapted for Proofs by Rewriting / rank @@
+Normal rank
@@ Property / cites work @@
+Structuring the verification of heap-manipulating programs
+Normal rank
@@ Property / cites work @@
+Q4783297
@@ Property / cites work: Q4783297 / rank @@
+Normal rank
@@ Property / cites work @@
+Types, bytes, and separation logic
@@ Property / cites work: Types, bytes, and separation logic / rank @@
+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 @@
+Relational separation logic
@@ Property / cites work: Relational separation logic / rank @@
+Normal rank
@@ Property / cites work @@
+Scalable Shape Analysis for Systems Code
@@ Property / cites work: Scalable Shape Analysis for Systems Code / rank @@
+Normal rank