@article(DBLP:journals/lmcs/AbdullaABN18,
 author       = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Ahmed Bouajjani and Tuan Phong Ngo},
 year         = {2018},
 title        = {A Load-Buffer Semantics for Total Store Ordering},
 journal      = {Log. Methods Comput. Sci.},
 volume       = {14},
 number       = {1},
 doi          = {10.23638/LMCS-14(1:9)2018},
)
@inproceedings(DBLP:conf/tacas/AbdullaACLR12,
 author       = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Yu{-}Fang Chen and Carl Leonardsson and Ahmed Rezine},
 year         = {2012},
 title        = {Counter-Example Guided Fence Insertion under {TSO}},
 editor       = {Cormac Flanagan and Barbara K{\"{o}}nig},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, {TACAS} 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7214},
 publisher    = {Springer},
 pages        = {204--219},
 doi          = {10.1007/978-3-642-28756-5\_15},
)
@inproceedings(DBLP:conf/icalp/AbdullaJ94,
 author       = {Parosh Aziz Abdulla and Bengt Jonsson},
 year         = {1994},
 title        = {Undecidable Verification Problems for Programs with Unreliable Channels},
 editor       = {Serge Abiteboul and Eli Shamir},
 booktitle    = {Automata, Languages and Programming, 21st International Colloquium, ICALP94, Jerusalem, Israel, July 11-14, 1994, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {820},
 publisher    = {Springer},
 pages        = {316--327},
 doi          = {10.1007/3-540-58201-0_78},
)
@article(wsts2,
 author       = {Parosh Aziz Abdulla and Bengt Jonsson},
 year         = {1996},
 title        = {Verifying Programs with Unreliable Channels},
 journal      = {Inf. Comput.},
 volume       = {127},
 number       = {2},
 pages        = {91--101},
 doi          = {10.1006/inco.1996.0053},
)
@inproceedings(DBLP:journals/corr/abs-2209-10319,
 author       = {Renato Acampora and Luca Geatti and Nicola Gigante and Angelo Montanari and Valentino Picotti},
 year         = {2022},
 title        = {Controller Synthesis for Timeline-based Games},
 editor       = {Pierre Ganty and Dario Della Monica},
 booktitle    = {Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2022, Madrid, Spain, September 21-23, 2022},
 series       = {{EPTCS}},
 volume       = {370},
 pages        = {131--146},
 doi          = {10.4204/EPTCS.370.9},
)
@manual(arm-v7ar-refman,
 organization = {ARM},
 year         = {2014},
 title        = {ARM Architecture Reference Manual, ARMv7-A and ARMv7-R edition},
 url          = {https://developer.arm.com/documentation/ddi0406/latest/},
)
@article(DBLP:journals/tcs/ArnoldVW03,
 author       = {Andr{\'{e}} Arnold and Aymeric Vincent and Igor Walukiewicz},
 year         = {2003},
 title        = {Games for synthesis of controllers with partial observation},
 journal      = {Theor. Comput. Sci.},
 volume       = {303},
 number       = {1},
 pages        = {7--34},
 doi          = {10.1016/S0304-3975(02)00442-5},
)
@article(DBLP:journals/siglog/Atig20,
 author       = {Mohamed Faouzi Atig},
 year         = {2020},
 title        = {What is decidable under the {TSO} memory model?},
 journal      = {{ACM} {SIGLOG} News},
 volume       = {7},
 number       = {4},
 pages        = {4--19},
 doi          = {10.1145/3458593.3458595},
)
@inproceedings(DBLP:conf/popl/AtigBBM10,
 author       = {Mohamed Faouzi Atig and Ahmed Bouajjani and Sebastian Burckhardt and Madanlal Musuvathi},
 year         = {2010},
 title        = {On the verification problem for weak memory models},
 editor       = {Manuel V. Hermenegildo and Jens Palsberg},
 booktitle    = {Proceedings of the 37th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2010, Madrid, Spain, January 17-23, 2010},
 publisher    = {{ACM}},
 pages        = {7--18},
 doi          = {10.1145/1706299.1706303},
)
@inproceedings(DBLP:conf/ecbs/BackS04,
 author       = {Ralph{-}Johan Back and Cristina Cerschi Seceleanu},
 year         = {2004},
 title        = {Contracts and Games in Controller Synthesis for Discrete Systems},
 booktitle    = {11th {IEEE} International Conference on the Engineering of Computer-Based Systems {(ECBS} 2004), 24-27 May 2004, Brno, Czech Republic},
 publisher    = {{IEEE} Computer Society},
 pages        = {307--315},
 doi          = {10.1109/ECBS.2004.1316713},
)
@inproceedings(DBLP:conf/adhs/BalkanVT15,
 author       = {Ayca Balkan and Moshe Y. Vardi and Paulo Tabuada},
 year         = {2015},
 title        = {Controller Synthesis for Mode-Target Games},
 editor       = {Magnus Egerstedt and Yorai Wardi},
 booktitle    = {5th {IFAC} Conference on Analysis and Design of Hybrid Systems, {ADHS} 2015, Atlanta, GA, USA, October 14-16, 2015},
 series       = {IFAC-PapersOnLine},
 volume       = {48},
 publisher    = {Elsevier},
 pages        = {343--350},
 doi          = {10.1016/J.IFACOL.2015.11.198},
)
@inproceedings(DBLP:conf/concur/BassetKW14,
 author       = {Nicolas Basset and Marta Z. Kwiatkowska and Clemens Wiltsche},
 year         = {2014},
 title        = {Compositional Controller Synthesis for Stochastic Games},
 editor       = {Paolo Baldan and Daniele Gorla},
 booktitle    = {{CONCUR} 2014 - Concurrency Theory - 25th International Conference, {CONCUR} 2014, Rome, Italy, September 2-5, 2014. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8704},
 publisher    = {Springer},
 pages        = {173--187},
 doi          = {10.1007/978-3-662-44584-6\_13},
)
@article(DBLP:journals/jacm/BrandZ83,
 author       = {Daniel Brand and Pitro Zafiropulo},
 year         = {1983},
 title        = {On Communicating Finite-State Machines},
 journal      = {J. {ACM}},
 volume       = {30},
 number       = {2},
 pages        = {323--342},
 doi          = {10.1145/322374.322380},
)
@article(wsts1,
 author       = {Alain Finkel and Philippe Schnoebelen},
 year         = {2001},
 title        = {Well-structured transition systems everywhere!},
 journal      = {Theor. Comput. Sci.},
 volume       = {256},
 number       = {1-2},
 pages        = {63--92},
 doi          = {10.1016/S0304-3975(00)00102-X},
)
@manual(power-isa-v31b,
 organization = {IBM},
 year         = {2021},
 title        = {Power ISA, Version 3.1b},
 url          = {https://files.openpower.foundation/s/dAYSdGzTfW4j2r2/download/OPF_PowerISA_v3.1B.pdf},
)
@manual(x86-swdmanual-1-3,
 organization = {Intel Corporation},
 year         = {2012},
 title        = {Intel 64 and IA-32 Architectures Software Developers Manual},
 url          = {https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html},
)
@article(DBLP:journals/tc/Lamport79,
 author       = {Leslie Lamport},
 year         = {1979},
 title        = {How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs},
 journal      = {{IEEE} Trans. Computers},
 volume       = {28},
 number       = {9},
 pages        = {690--691},
 doi          = {10.1109/TC.1979.1675439},
)
@inproceedings(DBLP:conf/dagstuhl/Mazala01,
 author       = {Ren{\'{e}} Mazala},
 year         = {2001},
 title        = {Infinite Games},
 editor       = {Erich Gr{\"{a}}del and Wolfgang Thomas and Thomas Wilke},
 booktitle    = {Automata, Logics, and Infinite Games: {A} Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]},
 series       = {Lecture Notes in Computer Science},
 volume       = {2500},
 publisher    = {Springer},
 pages        = {23--42},
 doi          = {10.1007/3-540-36387-4\_2},
)
@inproceedings(DBLP:conf/tphol/OwensSS09,
 author       = {Scott Owens and Susmit Sarkar and Peter Sewell},
 year         = {2009},
 title        = {A Better x86 Memory Model: x86-TSO},
 editor       = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
 booktitle    = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {391--407},
 doi          = {10.1007/978-3-642-03359-9\_27},
)
@article(DBLP:journals/ipl/Schnoebelen02,
 author       = {Philippe Schnoebelen},
 year         = {2002},
 title        = {Verifying lossy channel systems has nonprimitive recursive complexity},
 journal      = {Inf. Process. Lett.},
 volume       = {83},
 number       = {5},
 pages        = {251--261},
 doi          = {10.1016/S0020-0190(01)00337-4},
)
@article(DBLP:journals/cacm/SewellSONM10,
 author       = {Peter Sewell and Susmit Sarkar and Scott Owens and Francesco Zappa Nardelli and Magnus O. Myreen},
 year         = {2010},
 title        = {x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors},
 journal      = {Commun. {ACM}},
 volume       = {53},
 number       = {7},
 pages        = {89--97},
 doi          = {10.1145/1785414.1785443},
)
@manual(sparc9,
 organization = {SPARC International, Inc.},
 year         = {1994},
 title        = {{S}PARC {A}rchitecture {M}anual {V}ersion 9},
 url          = {https://sparc.org/wp-content/uploads/2014/01/SPARCV9.pdf.gz},
)
@misc(spengler2024reachability,
 author       = {Stephan Spengler},
 year         = {2024},
 title        = {Reachability and Safety Games under TSO Semantics (Extended Version)},
 eprint       = {2405.20804},
)
@inproceedings(DBLP:journals/corr/abs-2310-00990,
 author       = {Stephan Spengler and Sanchari Sil},
 year         = {2023},
 title        = {{TSO} Games - On the decidability of safety games under the total store order semantics},
 editor       = {Antonis Achilleos and Dario Della Monica},
 booktitle    = {Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2023, Udine, Italy, 18-20th September 2023},
 series       = {{EPTCS}},
 volume       = {390},
 pages        = {82--98},
 doi          = {10.4204/EPTCS.390.6},
)