{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T00:49:46Z","timestamp":1769042986970,"version":"3.49.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031562211","type":"print"},{"value":"9783031562228","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-56222-8_7","type":"book-chapter","created":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T08:02:30Z","timestamp":1710835350000},"page":"133-147","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On Verifying Concurrent Programs Under Weak Consistency Models: Decidability and\u00a0Complexity"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-662-46681-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353\u2013367. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Arora, J., Atig, M.F., Krishna, S.N.: Verification of programs under the release-acquire semantics. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22\u201326 June 2019, pp. 1117\u20131132. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314649","DOI":"10.1145\/3314221.3314649"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-030-67087-0_4","volume-title":"Networked Systems","author":"PA Abdulla","year":"2021","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Derevenetc, E., Leonardsson, C., Meyer, R.: On the state reachability problem for concurrent programs under power. In: Georgiou, C., Majumdar, R. (eds.) NETYS 2020. LNCS, vol. 12129, pp. 47\u201359. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67087-0_4"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: Context-bounded analysis for POWER. In: TACAS, pp. 56\u201374 (2017)","DOI":"10.1007\/978-3-662-54580-5_4"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: A load-buffer semantics for total store ordering. Logical Methods Comput. Sci. 14(1) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(1:9)2018","DOI":"10.23638\/LMCS-14(1:9)2018"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-41540-6_8","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless model checking for power. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 134\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_8"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. PACMPL 2(OOPSLA), 135:1\u2013135:29 (2018). https:\/\/doi.org\/10.1145\/3276505","DOI":"10.1145\/3276505"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-31277-0_1","volume-title":"Networked Systems","author":"PA Abdulla","year":"2019","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Dynamic partial order reduction under the release-acquire semantics (tutorial). In: Atig, M.F., Schwarzmann, A.A. (eds.) NETYS 2019. LNCS, vol. 11704, pp. 3\u201318. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31277-0_1"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Krishna, S., Gupta, A., Tuppe, O.: Optimal stateless model checking for causal consistency. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, 22\u201327 April 2023, Proceedings, Part I. LNCS, vol. 13993, pp. 105\u2013125. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_6","DOI":"10.1007\/978-3-031-30823-9_6"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1\u20137:74 (2014). https:\/\/doi.org\/10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain,17\u201323 January 2010. pp. 7\u201318. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706303","DOI":"10.1145\/1706299.1706303"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-28869-2_2","volume-title":"Programming Languages and Systems","author":"MF Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What\u2019s decidable about weak memory models? In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 26\u201346. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_2"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"MF Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99\u2013115. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_9"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-030-25543-5_17","volume-title":"Computer Aided Verification","author":"SM Beillahi","year":"2019","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Checking robustness against snapshot isolation. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 286\u2013304. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_17"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-030-72019-3_4","volume-title":"Programming Languages and Systems","author":"SM Beillahi","year":"2021","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Checking robustness between weak transactional consistency models. In: ESOP 2021. LNCS, vol. 12648, pp. 87\u2013117. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_4"},{"key":"7_CR16","unstructured":"Beillahi, S.M., Bouajjani, A., Enea, C.: Robustness against transactional causal consistency. Log. Methods Comput. Sci. 17(1) (2021). https:\/\/lmcs.episciences.org\/7149"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-642-37036-6_29","volume-title":"Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533\u2013553. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Enea, C., Rom\u00e1n-Calvo, E.: Dynamic partial order reduction for checking correctness against transaction isolation levels. Proc. ACM Program. Lang. 7(PLDI), 565\u2013590 (2023). https:\/\/doi.org\/10.1145\/3591243","DOI":"10.1145\/3591243"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-662-43951-7_14","volume-title":"Automata, Languages, and Programming","author":"E Derevenetc","year":"2014","unstructured":"Derevenetc, E., Meyer, R.: Robustness against power is PSpace-complete. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 158\u2013170. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43951-7_14"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Haas, T., Meyer, R., de Le\u00f3n, H.P.: CAAT: consistency as a theory. Proc. ACM Program. Lang. 6(OOPSLA2), 114\u2013144 (2022). https:\/\/doi.org\/10.1145\/3563292","DOI":"10.1145\/3563292"},{"key":"7_CR21","unstructured":"IBM: Power ISA, Version 2.07 (2013)"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. PACMPL 2, 17:1\u201317:32 (2018)","DOI":"10.1145\/3158105"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Lahav, O., Vafeiadis, V.: Kater: automating weak memory model metatheory and consistency checking. Proc. ACM Program. Lang. 7(POPL), 544\u2013572 (2023). https:\/\/doi.org\/10.1145\/3571212","DOI":"10.1145\/3571212"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Marmanis, I., Gladstein, V., Vafeiadis, V.: Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang. 6(POPL), 1\u201328 (2022). https:\/\/doi.org\/10.1145\/3498711","DOI":"10.1145\/3498711"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: Decidable verification under a causally consistent shared memory. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, 15\u201320 June 2020, pp. 211\u2013226. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385966","DOI":"10.1145\/3385412.3385966"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: What\u2019s decidable about causally consistent shared memory? ACM Trans. Program. Lang. Syst. 44(2), 8:1\u20138:55 (2022). https:\/\/doi.org\/10.1145\/3505273","DOI":"10.1145\/3505273"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Lahav, O., Margalit, R.: Robustness against release\/acquire semantics. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22\u201326 June 2019, pp. 126\u2013141. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314604","DOI":"10.1145\/3314221.3314604"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst. Des. 35(1), 73\u201397 (2009). https:\/\/doi.org\/10.1007\/S10703-009-0078-9","DOI":"10.1007\/S10703-009-0078-9"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Lamport, L.: How to make a multiprocessor that correctly executes multiprocess programs. IEEE Trans. Comput. C-28, 690\u2013691 (1979)","DOI":"10.1109\/TC.1979.1675439"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI. ACM (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_7"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, 4\u20138 June 2011, pp. 175\u2013186. ACM (2011)","DOI":"10.1145\/1993498.1993520"},{"issue":"7","key":"7_CR33","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-tso: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-02658-4_36","volume-title":"Computer Aided Verification","author":"S La Torre","year":"2009","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 477\u2013492. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_36"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Torre, S.L., Madhusudan, P., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: Hind, M., Diwan, A. (eds.) Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, 15\u201321 June 2009, pp. 211\u2013222. ACM (2009). https:\/\/doi.org\/10.1145\/1542476.1542500","DOI":"10.1145\/1542476.1542500"}],"container-title":["Lecture Notes in Computer Science","Taming the Infinities of Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-56222-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,6]],"date-time":"2024-11-06T22:02:50Z","timestamp":1730930570000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-56222-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031562211","9783031562228"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-56222-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"20 March 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}