@inproceedings{10.1007/978-3-030-72019-3_1,
    abstract = {We consider the reachability problem for finite-state multi-threaded programs under the promising semantics (PS 2.0) of Lee et al., which captures most common program transformations. Since reachability is already known to be undecidable in the fragment of PS 2.0 with only release-acquire accesses (PS 2.0-ra), we consider the fragment with only relaxed accesses and promises (PS 2.0-rlx). We show that reachability under PS 2.0-rlx is undecidable in general and that it becomes decidable, albeit non-primitive recursive, if we bound the number of promises.},
    address = {Cham},
    author = {Abdulla, Parosh Aziz
and Atig, Mohamed Faouzi
and Godbole, Adwait
and Krishna, S.
and Vafeiadis, Viktor},
    booktitle = {Programming Languages and Systems},
    date-added = {2023-11-7 9:40:16 +0100},
    editor = {Yoshida, Nobuko},
    isbn = {978-3-030-72019-3},
    pages = {1--29},
    publisher = {Springer International Publishing},
    title = {The Decidability of Verification under PS 2.0},
    year = {2021},
    doi = {10.1007/978-3-030-72019-3_1}
}

@inproceedings{10.1007/978-3-030-72019-3_1, abstract = {We consider the reachability problem for finite-state multi-threaded programs under the promising semantics (PS 2.0) of Lee et al., which captures most common program transformations. Since reachability is already known to be undecidable in the fragment of PS 2.0 with only release-acquire accesses (PS 2.0-ra), we consider the fragment with only relaxed accesses and promises (PS 2.0-rlx). We show that reachability under PS 2.0-rlx is undecidable in general and that it becomes decidable, albeit non-primitive recursive, if we bound the number of promises.}, address = {Cham}, author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Godbole, Adwait and Krishna, S. and Vafeiadis, Viktor}, booktitle = {Programming Languages and Systems}, date-added = {2023-11-7 9:40:16 +0100}, editor = {Yoshida, Nobuko}, isbn = {978-3-030-72019-3}, pages = {1--29}, publisher = {Springer International Publishing}, title = {The Decidability of Verification under PS 2.0}, year = {2021}, doi = {10.1007/978-3-030-72019-3_1} }