References

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

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org