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}
}

Search Results

Documents authored by Petitjean, Quentin

The Entailment Problem for Separation Logic with Overlaid Structures

Abstract

Cite as

Thanks for your feedback!

Could not send message