Proof tactics for assertions in separation logic (Q1687747): Difference between revisions

@@ Property / cites work @@
+Charge!
@@ Property / cites work: Charge! / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+On the Almighty Wand
@@ Property / cites work: On the Almighty Wand / rank @@
+Normal rank
@@ Property / cites work @@
+A Unified Display Proof Theory for Bunched Logic
@@ Property / cites work: A Unified Display Proof Theory for Bunched Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Undecidability of Propositional Separation Logic and Its Neighbours
+Normal rank
@@ Property / cites work @@
+Parametric completeness for separation theories
@@ Property / cites work: Parametric completeness for separation theories / rank @@
+Normal rank
@@ Property / cites work @@
+Compositional Shape Analysis by Means of Bi-Abduction
+Normal rank
@@ Property / cites work @@
+Computer Science Logic
@@ Property / cites work: Computer Science Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Effective interactive proofs for higher-order imperative programs
+Normal rank
@@ Property / cites work @@
+Local rely-guarantee reasoning
@@ Property / cites work: Local rely-guarantee reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Expressivity Properties of Boolean BI Through Relational Models
+Normal rank
@@ Property / cites work @@
+Q4411822
@@ Property / cites work: Q4411822 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof search for propositional abstract separation logics via labelled sequents
+Normal rank
@@ Property / cites work @@
+Automated Theorem Proving for Assertions in Separation Logic with All Connectives
+Normal rank
@@ Property / cites work @@
+A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
+Normal rank
@@ Property / cites work @@
+Completeness for a First-Order Abstract Separation Logic
+Normal rank
@@ Property / cites work @@
+Mechanised Separation Algebra
@@ Property / cites work: Mechanised Separation Algebra / rank @@
+Normal rank
@@ Property / cites work @@
+The Essence of Higher-Order Concurrent Separation Logic
+Normal rank
@@ Property / cites work @@
+Interactive proofs in higher-order concurrent separation logic
+Normal rank
@@ Property / cites work @@
+Nondeterministic Phase Semantics and the Undecidability of Boolean BI
+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 @@
+The Logic of Bunched Implications
@@ Property / cites work: The Logic of Bunched Implications / rank @@
+Normal rank
@@ Property / cites work @@
+A theorem prover for Boolean BI
@@ Property / cites work: A theorem prover for Boolean BI / rank @@
+Normal rank
@@ Property / cites work @@
+CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
+Normal rank
@@ Property / cites work @@
+A Formalisation of Smallfoot in HOL
@@ Property / cites work: A Formalisation of Smallfoot in HOL / 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 @@
+Higher-Order Separation Logic in Isabelle/HOLCF
@@ Property / cites work: Higher-Order Separation Logic in Isabelle/HOLCF / rank @@
+Normal rank