@article{10.1145/3434337,
    Abstract = {We address the problem of verifying the reachability problem in programs running under the formal model Px86 defined recently by Raad et al. in POPL'20 for the persistent Intel x86 architecture. We prove that this problem is decidable. To achieve that, we provide a new formal model that is equivalent to Px86 and that has the feature of being a well structured system. Deriving this new model is the result of a deep investigation of the properties of Px86 and the interplay of its components.},
    Address = {New York, NY, USA},
    Author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Bouajjani, Ahmed and Kumar, K. Narayan and Saivasan, Prakash},
    File = {Deciding Reachability under Persistent x86-TSO - 3434337 - a - t.pdf},
    Journal = {Proc. ACM Program. Lang.},
    Keywords = {program verification, TSO memory model, model checking, persistent memories},
    Month = {January},
    Number = {POPL},
    Publisher = {Association for Computing Machinery},
    Title = {Deciding Reachability under Persistent X86-TSO},
    URL = {https://doi.org/10.1145/3434337},
    Volume = {5},
    Year = {2021},
    articleno = {56},
    bdsk-url-1 = {https://doi.org/10.1145/3434337},
    date-added = {2021-01-13 14:20:20 +0100},
    date-modified = {2021-01-13 14:20:20 +0100},
    issue_date = {January 2021},
    numpages = {32},
    doi = {10.1145/3434337}
}

@article{10.1145/3434337, Abstract = {We address the problem of verifying the reachability problem in programs running under the formal model Px86 defined recently by Raad et al. in POPL'20 for the persistent Intel x86 architecture. We prove that this problem is decidable. To achieve that, we provide a new formal model that is equivalent to Px86 and that has the feature of being a well structured system. Deriving this new model is the result of a deep investigation of the properties of Px86 and the interplay of its components.}, Address = {New York, NY, USA}, Author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Bouajjani, Ahmed and Kumar, K. Narayan and Saivasan, Prakash}, File = {Deciding Reachability under Persistent x86-TSO - 3434337 - a - t.pdf}, Journal = {Proc. ACM Program. Lang.}, Keywords = {program verification, TSO memory model, model checking, persistent memories}, Month = {January}, Number = {POPL}, Publisher = {Association for Computing Machinery}, Title = {Deciding Reachability under Persistent X86-TSO}, URL = {https://doi.org/10.1145/3434337}, Volume = {5}, Year = {2021}, articleno = {56}, bdsk-url-1 = {https://doi.org/10.1145/3434337}, date-added = {2021-01-13 14:20:20 +0100}, date-modified = {2021-01-13 14:20:20 +0100}, issue_date = {January 2021}, numpages = {32}, doi = {10.1145/3434337} }