2026-07-23T03:28:47Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25440 2026-03-19T13:28:33Z ddc:004 open_access

On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions Peltier, Nicolas Separation logic Dynamic logic Entailment problem Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules - known as PCE (Progressing, Connected, and Established) - has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nicolas Peltier 2026 Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2026.16 urn:nbn:de:0030-drops-254402 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.16 eng https://creativecommons.org/licenses/by/4.0/legalcode