A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions (Q5875940): Difference between revisions

Latest revision as of 11:58, 31 July 2024

scientific article; zbMATH DE number 7650597

Language	Label	Description	Also known as
English	A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions	scientific article; zbMATH DE number 7650597

Statements

instance of

scholarly article

0 references

title

A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions (English)

0 references

0 references

0 references

0 references

0 references

ACM Transactions on Computational Logic

0 references

publication date

7 February 2023

0 references

full work available at URL

https://arxiv.org/abs/2002.01202

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

decision procedures

0 references

entailment

0 references

magic wands

0 references

inductive predicates

0 references

0 references

0 references

0 references

Foundations for Decision Problems in Separation Logic with General Inductive Predicates

0 references

Program Logics for Certified Compilers

0 references

Q3292904

0 references

Shape Analysis for Composite Data Structures

0 references

FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science

0 references

Programming Languages and Systems

0 references

On the almighty wand

0 references

Formalised Inductive Reasoning in the Logic of Bunched Implications

0 references

Automated Cyclic Entailment Proofs in Separation Logic

0 references

A decision procedure for satisfiability in separation logic with inductive predicates

0 references

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic

0 references

Compositional Shape Analysis by Means of Bi-Abduction

0 references

Q4474211

0 references

Automated verification of shape, size and bag properties via user-defined predicates in separation logic

0 references

Tractable Reasoning in a Fragment of Separation Logic

0 references

Q3077955

0 references

Constructive versions of Tarski's fixed point theorems

0 references

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates

0 references

Unifying decidable entailments in separation logic with inductive definitions

0 references

Q4506483

0 references

The Tree Width of Separation Logic with Recursive Definitions

0 references

Deciding Entailments in Inductive Separation Logic with Tree Automata

0 references

BI as an assertion language for mutable data structures

0 references

Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

0 references

Iris from the ground up: A modular foundation for higher-order concurrent separation logic

0 references

A decidable fragment in separation logic with inductive predicates and arithmetic

0 references

Viper: A Verification Infrastructure for Permission-Based Reasoning

0 references

Automated mutual explicit induction proof in separation logic

0 references

Automated mutual induction proof in separation logic

0 references

describes a project that uses

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

MaRDI publication profile

0 references

OpenAlex ID

W4296613475

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:5875940

@@ Property / cites work @@
+HIP
@@ Property / cites work: HIP / rank @@
+Normal rank
@@ Property / cites work @@
+Smallfoot
@@ Property / cites work: Smallfoot / rank @@
+Normal rank
@@ Property / cites work @@
+GRASShopper
@@ Property / cites work: GRASShopper / rank @@
+Normal rank
@@ Property / cites work @@
+Foundations for Decision Problems in Separation Logic with General Inductive Predicates
+Normal rank
@@ Property / cites work @@
+Program Logics for Certified Compilers
@@ Property / cites work: Program Logics for Certified Compilers / rank @@
+Normal rank
@@ Property / cites work @@
+Q3292904
@@ Property / cites work: Q3292904 / rank @@
+Normal rank
@@ Property / cites work @@
+Shape Analysis for Composite Data Structures
@@ Property / cites work: Shape Analysis for Composite Data Structures / 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 @@
+On the almighty wand
@@ Property / cites work: On the almighty wand / rank @@
+Normal rank
@@ Property / cites work @@
+Formalised Inductive Reasoning in the Logic of Bunched Implications
+Normal rank
@@ Property / cites work @@
+Automated Cyclic Entailment Proofs in Separation Logic
+Normal rank
@@ Property / cites work @@
+A decision procedure for satisfiability in separation logic with inductive predicates
+Normal rank
@@ Property / cites work @@
+Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
+Normal rank
@@ Property / cites work @@
+Compositional Shape Analysis by Means of Bi-Abduction
+Normal rank
@@ Property / cites work @@
+Q4474211
@@ Property / cites work: Q4474211 / 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 @@
+Tractable Reasoning in a Fragment of Separation Logic
+Normal rank
@@ Property / cites work @@
+Q3077955
@@ Property / cites work: Q3077955 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive versions of Tarski's fixed point theorems
+Normal rank
@@ Property / cites work @@
+The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates
+Normal rank
@@ Property / cites work @@
+Unifying decidable entailments in separation logic with inductive definitions
+Normal rank
@@ Property / cites work @@
+Q4506483
@@ Property / cites work: Q4506483 / rank @@
+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 @@
+Iris from the ground up: A modular foundation for higher-order concurrent separation logic
+Normal rank
@@ Property / cites work @@
+A decidable fragment in separation logic with inductive predicates and arithmetic
+Normal rank
@@ Property / cites work @@
+Viper: A Verification Infrastructure for Permission-Based Reasoning
+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
@@ Property / describes a project that uses @@
+HIP
@@ Property / describes a project that uses: HIP / rank @@
+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 @@
+Viper
@@ Property / describes a project that uses: Viper / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Slide
@@ Property / describes a project that uses: Slide / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Infer
@@ Property / describes a project that uses: Infer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Toolchain
@@ Property / describes a project that uses: Toolchain / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SLAyer
@@ Property / describes a project that uses: SLAyer / 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 / OpenAlex ID @@
+W4296613475
@@ Property / OpenAlex ID: W4296613475 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5875940