A proof procedure for separation logic with inductive definitions and data

DOI10.1007/S10817-023-09680-4MaRDI QIDQ6053843zbMATH OpenFDO

Authors Mnacho Echenim, Nicolas Peltier

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

entailment probleminductive theorem provingseparation logictheory reasoning

Mathematics Subject Classification ID

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

Abstract: A proof procedure, in the spirit of the sequent calculus, is proposed to check the validity of entailments between Separation Logic formulas combining inductively defined predicates denoted structures of bounded tree width and theory reasoning. The calculus is sound and complete, in the sense that a sequent is valid iff it admits a (possibly infinite) proof tree. We show that the procedure terminates in the two following cases: (i) When the inductive rules that define the predicates occurring on the left-hand side of the entailment terminate, in which case the proof tree is always finite. (ii) When the theory is empty, in which case every valid sequent admits a rational proof tree, where the total number of pairwise distinct sequents occurring in the proof tree is doubly exponential w.r.t. the size of the end-sequent.

Cites work

• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• Compositional entailment checking for a fragment of separation logic
• Compositional satisfiability solving in separation logic
• Compositional shape analysis by means of bi-abduction
• Deciding entailments in inductive separation logic with tree automata
• From Separation Logic to Hyperedge Replacement and Back
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Generating inductive predicates for symbolic execution of pointer-manipulating programs
• Haskell overloading is DEXPTIME-complete
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Labelled cyclic proofs for separation logic
• Satisfiability of compositional separation logic with tree predicates and data constraints
• Separation logic modulo theories
• Separation logic with one quantified variable
• Sequent calculi for induction and infinite descent
• The tree width of separation logic with recursive definitions
• Tractable Reasoning in a Fragment of Separation Logic

Cited in

(7)

• Unifying decidable entailments in separation logic with inductive definitions
• Separation logic with linearly compositional inductive predicates and set data constraints
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• Restriction on cut rule in cyclic-proof system for symbolic heaps
• Tractable and intractable entailment problems in separation logic with inductively defined predicates
• A direct procedure to test entailment in a separation logic of relations
• An EXPTIME-complete entailment problem in separation logic

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6053843)