The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains

Abstract : This paper investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications , for prenex formulae with quantifier prefix ∃ * ∀ *. In analogy with first-order logic, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [BSR(SL k)]. In contrast to existing work in Separation Logic, in which the universe of possible locations is assumed to be infinite, both finite and infinite universes are considered. We show that, unlike in first-order logic, the (in)finite sat-isfiability problem is undecidable for BSR(SL k). Then we define two non-trivial subsets thereof, that are decidable for finite and infinite satisfiability respectively, by controlling the occurrences of universally quantified variables within the scope of separating implications, as well as the polarity of the occurrences of the latter. Beside the theoretical interest, our work has natural applications in program verification, for checking that constraints on the shape of a data-structure are preserved by a sequence of transformations.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-02094154
Contributor : Nicolas Peltier <>
Submitted on : Tuesday, November 5, 2019 - 10:05:29 AM
Last modification on : Thursday, November 7, 2019 - 11:39:07 AM

File

paper_9 (1).pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. Foundations of Software Science and Computation Structures (FOSSACS) - 22nd International Conference, 2019, Prague, Czech Republic. pp.242-259, ⟨10.1007/978-3-030-17127-8_14⟩. ⟨hal-02094154⟩

Share

Metrics

Record views

56

Files downloads

47