Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Separation Logic with One Quantified Variable
verfasst von : Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry
Erschienen in: Computer Science - Theory and Applications
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We investigate first-order separation logic with one record field restricted to a unique quantified variable (1SL1). Undecidability is known when the number of quantified variables is unbounded and the satisfiability problem is
pspace
-complete for the propositional fragment. We show that the satisfiability problem for 1SL1 is
pspace
-complete and we characterize its expressive power by showing that every formula is equivalent to a Boolean combination of atomic properties. This contributes to our understanding of fragments of first-order separation logic that can specify properties about the memory heap of programs with singly-linked lists. When the number of program variables is fixed, the complexity drops to polynomial time. All the fragments we consider contain the magic wand operator and first-order quantification over a single variable.