Completeness and expressiveness of pointer program verification by separation logic (Q2417849): Difference between revisions

@@ Property / cites work @@
+Completeness for recursive procedures in separation logic
+Normal rank
@@ Property / cites work @@
+Ten Years of Hoare's Logic: A Survey—Part I
@@ Property / cites work: Ten Years of Hoare's Logic: A Survey—Part I / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Expressiveness and the completeness of Hoare's logic
+Normal rank
@@ Property / cites work @@
+Formalised Inductive Reasoning in the Logic of Bunched Implications
+Normal rank
@@ Property / cites work @@
+Cyclic proofs of program termination in separation logic
+Normal rank
@@ Property / cites work @@
+Automated Cyclic Entailment Proofs in Separation Logic
+Normal rank
@@ Property / cites work @@
+Foundations of Software Science and Computational Structures
+Normal rank
@@ Property / cites work @@
+Context logic as modal logic
@@ Property / cites work: Context logic as modal logic / rank @@
+Normal rank
@@ Property / cites work @@
+Automated verification of shape, size and bag properties via user-defined predicates in separation logic
+Normal rank
@@ Property / cites work @@
+Soundness and Completeness of an Axiom System for Program Verification
+Normal rank
@@ Property / cites work @@
+Q5753923
@@ Property / cites work: Q5753923 / rank @@
+Normal rank
@@ Property / cites work @@
+Lifting abstract interpreters to quantified logical domains
+Normal rank
@@ Property / cites work @@
+BI as an assertion language for mutable data structures
+Normal rank
@@ Property / cites work @@
+Q3334976
@@ Property / cites work: Q3334976 / rank @@
+Normal rank
@@ Property / cites work @@
+Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types
+Normal rank
@@ Property / cites work @@
+Elimination of spatial connectives in static spatial logics
+Normal rank
@@ Property / cites work @@
+Automated Verification of Shape and Size Properties Via Separation Logic
+Normal rank
@@ Property / cites work @@
+Enhancing Program Verification with Lemmas
@@ Property / cites work: Enhancing Program Verification with Lemmas / rank @@
+Normal rank
@@ Property / cites work @@
+Q3773877
@@ Property / cites work: Q3773877 / rank @@
+Normal rank
@@ Property / cites work @@
+Program synthesis using realizability
@@ Property / cites work: Program synthesis using realizability / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Science Logic
@@ Property / cites work: Computer Science Logic / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q128273622
@@ Property / Wikidata QID: Q128273622 / rank @@
+Normal rank