@inproceedings{10.1007/978-3-030-17127-8_14,
    Abstract = {This paper investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications, for prenex formul{\ae} with quantifier prefix {\$}{\$}{\backslash}exists ^*{\backslash}forall ^*{\$}{\$}. In analogy with first-order logic, we call this fragment Bernays-Sch{\"o}nfinkel-Ramsey Separation Logic [{\$}{\$}{\backslash}mathsf {\{}BSR{\}}({\backslash}mathsf {\{}SL{\}}^{\{}{\backslash}!{\backslash}scriptstyle {\{}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 satisfiability problem is undecidable for {\$}{\$}{\backslash}mathsf {\{}BSR{\}}({\backslash}mathsf {\{}SL{\}}^{\{}{\backslash}!{\backslash}scriptstyle {\{}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.},
    Address = {Cham},
    Author = {Echenim, Mnacho and Iosif, Radu and Peltier, Nicolas},
    BookTitle = {Foundations of Software Science and Computation Structures},
    Editor = {Boja{\'{n}}czyk, Miko{{\l}}aj and Simpson, Alex},
    File = {Echenim2019\_Chapter\_TheBernays-Schönfinkel-RamseyC (0) - a - a - d.pdf},
    ISBN = {978-3-030-17127-8},
    Pages = {242--259},
    Publisher = {Springer International Publishing},
    Title = {The Bernays-Sch{\"o}nfinkel-Ramsey Class of Separation Logic on Arbitrary Domains},
    Year = {2019},
    date-added = {2019-04-11 15:31:13 +0200},
    date-modified = {2019-04-11 15:31:13 +0200},
    doi = {10.1007/978-3-030-17127-8_14}
}

@inproceedings{10.1007/978-3-030-17127-8_14, Abstract = {This paper investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications, for prenex formul{\ae} with quantifier prefix {\$}{\$}{\backslash}exists ^{\backslash}forall ^, Address = {Cham}, Author = {Echenim, Mnacho and Iosif, Radu and Peltier, Nicolas}, BookTitle = {Foundations of Software Science and Computation Structures}, Editor = {Boja{\'{n}}czyk, Miko{{\l}}aj and Simpson, Alex}, File = {Echenim2019_Chapter_TheBernays-Schönfinkel-RamseyC (0) - a - a - d.pdf}, ISBN = {978-3-030-17127-8}, Pages = {242--259}, Publisher = {Springer International Publishing}, Title = {The Bernays-Sch{\"o}nfinkel-Ramsey Class of Separation Logic on Arbitrary Domains}, Year = {2019}, date-added = {2019-04-11 15:31:13 +0200}, date-modified = {2019-04-11 15:31:13 +0200}, doi = {10.1007/978-3-030-17127-8_14} }}{\$}. In analogy with first-order logic, we call this fragment Bernays-Sch{\"o}nfinkel-Ramsey Separation Logic [{\$}{\$}{\backslash}mathsf {{}BSR{}}({\backslash}mathsf {{}SL{}}^{{}{\backslash}!{\backslash}scriptstyle {{}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 satisfiability problem is undecidable for {\$}{\$}{\backslash}mathsf {{}BSR{}}({\backslash}mathsf {{}SL{}}^{{}{\backslash}!{\backslash}scriptstyle {{}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.