A First-Order Logic with Frames (Q5041109): Difference between revisions

@@ Property / cites work @@
+Local Reasoning for Global Invariants, Part II
@@ Property / cites work: Local Reasoning for Global Invariants, Part II / rank @@
+Normal rank
@@ Property / cites work @@
+Local Reasoning for Global Invariants, Part I
@@ Property / cites work: Local Reasoning for Global Invariants, Part I / rank @@
+Normal rank
@@ Property / cites work @@
+FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Analysis of algorithms on threaded trees
@@ Property / cites work: Analysis of algorithms on threaded trees / 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 @@
+Automated Cyclic Entailment Proofs in Separation Logic
+Normal rank
@@ Property / cites work @@
+Tractable Reasoning in a Fragment of Separation Logic
+Normal rank
@@ Property / cites work @@
+Separation logics and modalities: a survey
@@ Property / cites work: Separation logics and modalities: a survey / rank @@
+Normal rank
@@ Property / cites work @@
+Modular reasoning about heap paths via effectively propositional formulas
+Normal rank
@@ Property / cites work @@
+The dynamic frames theory
@@ Property / cites work: The dynamic frames theory / rank @@
+Normal rank
@@ Property / cites work @@
+Coming to terms with quantified reasoning
@@ Property / cites work: Coming to terms with quantified reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+A Basis for Verifying Multi-threaded Programs
@@ Property / cites work: A Basis for Verifying Multi-threaded Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Recursive proofs for inductive tree data-structures
+Normal rank
@@ Property / cites work @@
+Q4783297
@@ Property / cites work: Q4783297 / rank @@
+Normal rank
@@ Property / cites work @@
+Separation and information hiding
@@ Property / cites work: Separation and information hiding / rank @@
+Normal rank
@@ Property / cites work @@
+Separation logic and abstraction
@@ Property / cites work: Separation logic and abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+The Relationship between Separation Logic and Implicit Dynamic Frames
+Normal rank
@@ Property / cites work @@
+Separation Logic Modulo Theories
@@ Property / cites work: Separation Logic Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Decision procedures for algebraic data types with abstractions
+Normal rank
@@ Property / cites work @@
+Automated mutual explicit induction proof in separation logic
+Normal rank
@@ Property / describes a project that uses @@
+Smallfoot
@@ Property / describes a project that uses: Smallfoot / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+GRASShopper
@@ Property / describes a project that uses: GRASShopper / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Dafny
@@ Property / describes a project that uses: Dafny / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VAMPIRE
@@ Property / describes a project that uses: VAMPIRE / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3021453356
@@ Property / OpenAlex ID: W3021453356 / rank @@
+Normal rank