{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:24:43Z","timestamp":1779074683802,"version":"3.51.4"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961415","type":"print"},{"value":"9783319961422","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96142-2_21","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T15:55:08Z","timestamp":1532102108000},"page":"336-353","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Reasoning About TSO Programs Using Reduction and Abstraction"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suha Orhun","family":"Mutluergil","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-28756-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2012","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 204\u2013219. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_15"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-662-46669-8_13","volume-title":"Programming Languages and Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Atig, M.F., Ngo, T.-P.: The best of both worlds: trading efficiency and optimality in fence insertion for TSO. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 308\u2013332. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_13"},{"issue":"6","key":"21_CR3","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1109\/71.242161","volume":"4","author":"SV Adve","year":"1993","unstructured":"Adve, S.V., Hill, M.D.: A unified formalization of four shared-memory models. IEEE Trans. Parallel Distrib. Syst. 4(6), 613\u2013624 (1993)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-319-08867-9_33","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don\u2019t sit on the fence. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 508\u2013524. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_33"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-22110-1_6","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L.: Stability in weak memory models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 50\u201366. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_6"},{"issue":"1","key":"21_CR6","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/1707801.1706303","volume":"45","author":"MF Atig","year":"2010","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. ACM Sigplan Not. 45(1), 7\u201318 (2010)","journal-title":"ACM Sigplan Not."},{"key":"21_CR7","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":"21_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Enea, C., Mutluergil, S.O., Tasiran, S.: Reasoning about TSO programs using reduction and abstraction. CoRR, abs\/1804.05196 (2018)","DOI":"10.1007\/978-3-319-96142-2_21"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-642-22012-8_34","volume-title":"Automata, Languages and Programming","author":"A Bouajjani","year":"2011","unstructured":"Bouajjani, A., Meyer, R., M\u00f6hlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 428\u2013440. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22012-8_34"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-70545-1_12","volume-title":"Computer Aided Verification","author":"S Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 107\u2013120. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_12"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-642-19835-9_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Burnim","year":"2011","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 11\u201325. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_3"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: ACM Symposium on Principles of Programming Languages, p. 14. Association for Computing Machinery Inc., January 2009","DOI":"10.1145\/1594834.1480885"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: Computer Aided Verification (2015)","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: ACM SIGPLAN Notices, vol. 46, pp. 187\u2013198. ACM (2011)","DOI":"10.1145\/1993498.1993521"},{"issue":"2","key":"21_CR15","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1145\/2261417.2261438","volume":"43","author":"M Kuperstein","year":"2012","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. ACM SIGACT News 43(2), 108\u2013123 (2012)","journal-title":"ACM SIGACT News"},{"issue":"9","key":"21_CR16","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"100","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 100(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"issue":"12","key":"21_CR17","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-14107-2_23","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"S Owens","year":"2010","unstructured":"Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 478\u2013503. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_23"},{"issue":"7","key":"21_CR19","doi-asserted-by":"crossref","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"},{"issue":"2","key":"21_CR20","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D Shasha","year":"1988","unstructured":"Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. (TOPLAS) 10(2), 282\u2013312 (1988)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96142-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T23:20:44Z","timestamp":1571613644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96142-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961415","9783319961422"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96142-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}