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/LIPIcs.CONCUR.2022.24

On an Invariance Problem for Parameterized Concurrent Systems

Authors: Marius Bozga, Lucas Bueri, and Radu Iosif

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract

We consider concurrent systems consisting of replicated finite-state processes that synchronize via joint interactions in a network with user-defined topology. The system is specified using a resource logic with a multiplicative connective and inductively defined predicates, reminiscent of Separation Logic [John C. Reynolds, 2002]. The problem we consider is if a given formula in this logic defines an invariant, namely whether any model of the formula, following an arbitrary firing sequence of interactions, is transformed into another model of the same formula. This property, called havoc invariance, is quintessential in proving the correctness of reconfiguration programs that change the structure of the network at runtime. We show that the havoc invariance problem is many-one reducible to the entailment problem ϕ ⊧ ψ, asking if any model of ϕ is also a model of ψ. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.

Cite as

Marius Bozga, Lucas Bueri, and Radu Iosif. On an Invariance Problem for Parameterized Concurrent Systems. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bozga_et_al:LIPIcs.CONCUR.2022.24,
  author =	{Bozga, Marius and Bueri, Lucas and Iosif, Radu},
  title =	{{On an Invariance Problem for Parameterized Concurrent Systems}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.24},
  URN =		{urn:nbn:de:0030-drops-170874},
  doi =		{10.4230/LIPIcs.CONCUR.2022.24},
  annote =	{Keywords: parameterized verification, invariant checking, resource logics, reconfigurable systems, tree automata}
}

Search Results

Documents authored by Bueri, Lucas

The Entailment Problem for Separation Logic with Overlaid Structures

Abstract

Cite as

On an Invariance Problem for Parameterized Concurrent Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message