A proof procedure for separation logic with inductive definitions and data

DOI10.1007/s10817-023-09680-4arXiv2201.13227MaRDI QIDQ6053843

Nicolas Peltier, Mnacho Echenim

Publication date: 24 October 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2201.13227

zbMATH Keywords

inductive theorem provingseparation logictheory reasoningentailment problem

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Haskell overloading is DEXPTIME-complete
• Compositional entailment checking for a fragment of separation logic
• Compositional satisfiability solving in separation logic
• Satisfiability of compositional separation logic with tree predicates and data constraints
• Separation Logic Modulo Theories
• Tractable Reasoning in a Fragment of Separation Logic
• Sequent calculi for induction and infinite descent
• Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs
• Labelled cyclic proofs for separation logic
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• From Separation Logic to Hyperedge Replacement and Back
• The Tree Width of Separation Logic with Recursive Definitions
• Separation Logic with One Quantified Variable
• Compositional Shape Analysis by Means of Bi-Abduction
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

This page was built for publication: A proof procedure for separation logic with inductive definitions and data