Name
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.
|
Year | DOI | Venue |
|---|---|---|
2021 | 10.1145/3434337 | Proceedings of the ACM on Programming Languages |
Keywords | DocType | Volume |
TSO memory model,model checking,persistent memories,program verification | Journal | 5 |
Issue | ISSN | Citations |
POPL | 2475-1421 | 1 |
PageRank | References | Authors |
0.35 | 20 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Parosh Aziz Abdulla | 1 | 2010 | 122.22 |
| Mohamed Faouzi Atig | 2 | 505 | 40.94 |
| Ahmed Bouajjani | 3 | 2663 | 184.84 |
| K. Narayan Kumar | 4 | 74 | 7.24 |
| Prakash Saivasan | 5 | 34 | 7.49 |