Effective entailment checking for separation logic with inductive definitions

DOI10.1007/978-3-030-17465-1_18MaRDI QIDQ6091412zbMATH OpenFDO

Authors Jens Katelaan, Christoph Matheja, Florian Zuleger

Publication date 24 November 2023

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-17465-1_18

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Deciding entailments in inductive separation logic with tree automata
• A complete decision procedure for linearly compositional separation logic with data constraints
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic

Cited in

(8)

• Foundations for entailment checking in quantitative separation logic
• Beyond symbolic heaps: deciding separation logic with inductive definitions
• Entailment checking in separation logic with inductive definitions is 2-ExpTime hard
• Tree-verifiable graph grammars
• Decidable entailments in separation logic with inductive definitions: beyond establishment
• Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
• Unifying decidable entailments in separation logic with inductive definitions
• Completeness of cyclic proofs for symbolic heaps with inductive definitions

This page was built for publication: Effective entailment checking for separation logic with inductive definitions

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