An efficient cyclic entailment procedure in a fragment of separation logic (Q6091213): Difference between revisions

@@ Property / cites work @@
+Foundations for Decision Problems in Separation Logic with General Inductive Predicates
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning with Analytic Tableaux and Related Methods
+Normal rank
@@ Property / cites work @@
+Automated Cyclic Entailment Proofs in Separation Logic
+Normal rank
@@ Property / cites work @@
+Compositional shape analysis by means of bi-abduction
+Normal rank
@@ Property / cites work @@
+Q5111651
@@ Property / cites work: Q5111651 / rank @@
+Normal rank
@@ Property / cites work @@
+Tractable Reasoning in a Fragment of Separation Logic
+Normal rank
@@ Property / cites work @@
+Unifying decidable entailments in separation logic with inductive definitions
+Normal rank
@@ Property / cites work @@
+Compositional entailment checking for a fragment of separation logic
+Normal rank
@@ Property / cites work @@
+On Automated Lemma Generation for Separation Logic with Inductive Definitions
+Normal rank
@@ Property / cites work @@
+A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
+Normal rank
@@ Property / cites work @@
+The Tree Width of Separation Logic with Recursive Definitions
+Normal rank
@@ Property / cites work @@
+Deciding Entailments in Inductive Separation Logic with Tree Automata
+Normal rank
@@ Property / cites work @@
+BI as an assertion language for mutable data structures
+Normal rank
@@ Property / cites work @@
+Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
+Normal rank
@@ Property / cites work @@
+A separation logic with data: small models and automation
+Normal rank
@@ Property / cites work @@
+A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
+Normal rank
@@ Property / cites work @@
+Compositional satisfiability solving in separation logic
+Normal rank
@@ Property / cites work @@
+A decision procedure for string logic with quadratic equations, regular expressions and length constraints
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Heap-Based Programs
@@ Property / cites work: Satisfiability Modulo Heap-Based Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Frame inference for inductive entailment proofs in separation logic
+Normal rank
@@ Property / cites work @@
+A decidable fragment in separation logic with inductive predicates and arithmetic
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Separation Logic Modulo Theories
@@ Property / cites work: Separation Logic Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Automated mutual explicit induction proof in separation logic
+Normal rank
@@ Property / cites work @@
+Automated mutual induction proof in separation logic
+Normal rank