DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2026.94

The Entailment Problem for Separation Logic with Overlaid Structures

Authors: Lucas Bueri, Nicolas Peltier, Quentin Petitjean, and Mihaela Sighireanu

Published in: LIPIcs, Volume 386, 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)

Abstract

Separation Logic (SL) enables reasoning about programs that manipulate pointers. Its key feature is the separating conjunction ⋆, which asserts that two formulas hold on disjoint portions of memory. We consider an extension of SL, called Overlaid SL (OSL), that allows non-disjoint combinations of data structures defined over different fields, enriched with set constraints on the nodes of these structures. We prove that entailment is decidable for a broad class of data structures satisfying the so-called PCE conditions of [Iosif et al., 2013], thus extending this result to OSL. Our decision procedure is nondeterministic with doubly exponential time complexity.

Cite as

Lucas Bueri, Nicolas Peltier, Quentin Petitjean, and Mihaela Sighireanu. The Entailment Problem for Separation Logic with Overlaid Structures. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 94:1-94:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bueri_et_al:LIPIcs.MFCS.2026.94,
  author =	{Bueri, Lucas and Peltier, Nicolas and Petitjean, Quentin and Sighireanu, Mihaela},
  title =	{{The Entailment Problem for Separation Logic with Overlaid Structures}},
  booktitle =	{51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)},
  pages =	{94:1--94:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-442-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{386},
  editor =	{Kouck\'{y}, Michal and Petrișan, Daniela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2026.94},
  URN =		{urn:nbn:de:0030-drops-274766},
  doi =		{10.4230/LIPIcs.MFCS.2026.94},
  annote =	{Keywords: Decision Procedure, Separation Logic, Inductive Definitions, Overlaid Data Structures}
}

Document

DOI: 10.4230/DROPS.MEMICS.2009.2356

Rewriting Systems over Nested Data Words

Authors: Ahmed Bouajjani, Cezara Drăgoi, Yan Jurski, and Mihaela Sighireanu

Published in: OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009)

Abstract

We propose a generic framework for reasoning about infinite state systems handling data like integers, booleans etc. and having complex control structures. We consider that configurations of such systems are represented by nested data words, i.e., words of ... words over a potentially infinite data domain. We define a logic called $\ndwl$ allowing to reason about nested data words, and we define rewriting systems called $\ndwrs$ over these nested structures. The rewriting systems are constrained by formulas in the logic specifying the rewriting positions as well as structure/data transformations. We define a fragment $\Sigma_2^*$ of $\ndwl$ with a decidable satisfiability problem. Moreover, we show that the transition relation defined by rewriting systems with $\Sigma_2^*$ constraints can be effectively defined in the same fragment. These results can be used in the automatization of verification problems such as inductive invariance checking and bounded reachability analysis. Our framework allows to reason about a wide range of concurrent systems including multithreaded programs (with procedure calls, thread creation, global/local variables over infinite data domains, locks, monitors, etc.), dynamic networks of timed systems, cache coherence/mutex/communication protocols, etc.

Cite as

Ahmed Bouajjani, Cezara Drăgoi, Yan Jurski, and Mihaela Sighireanu. Rewriting Systems over Nested Data Words. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 70-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bouajjani_et_al:OASIcs:2009:DROPS.MEMICS.2009.2356,
  author =	{Bouajjani, Ahmed and Dr\u{a}goi, Cezara and Jurski, Yan and Sighireanu, Mihaela},
  title =	{{Rewriting Systems over Nested Data Words}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{70--79},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2356},
  URN =		{urn:nbn:de:0030-drops-23567},
  doi =		{10.4230/DROPS.MEMICS.2009.2356},
  annote =	{Keywords: Nested data words, rewriting systems, program verification, dynamic and parametrized systems, invariance checking}
}

Search Results

Documents authored by Sighireanu, Mihaela

The Entailment Problem for Separation Logic with Overlaid Structures

Abstract

Cite as

Rewriting Systems over Nested Data Words

Abstract

Cite as

Thanks for your feedback!

Could not send message