{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:15:28Z","timestamp":1748751328807,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662491911"},{"type":"electronic","value":"9783662491928"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49192-8_33","type":"book-chapter","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T15:47:27Z","timestamp":1452181647000},"page":"404-417","source":"Crossref","is-referenced-by-count":1,"title":["Bounded TSO-to-SC Linearizability Is Decidable"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[]},{"given":"Yi","family":"Lv","sequence":"additional","affiliation":[]},{"given":"Peng","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,1,8]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. In: LICS 1996, pp. 219\u2013228. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561322"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Hermenegildo, M., et al. (eds.) POPL 2010, pp. 7\u201318. ACM (2010)","DOI":"10.1145\/1707801.1706303"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C\/C++ concurrency. In: Giacobazzi, R., Cousot, R. (eds.) POPL 2013, pp. 235\u2013248. ACM (2013)","DOI":"10.1145\/2480359.2429099"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-37036-6_17","volume-title":"Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 290\u2013309. Springer, Heidelberg (2013)"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-662-47666-6_8","volume-title":"Automata, Languages, and Programming","author":"A Bouajjani","year":"2015","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: On reducing linearizability to state reachability. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 95\u2013107. Springer, Heidelberg (2015)"},{"issue":"1","key":"33_CR6","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1145\/2775051.2677002","volume":"50","author":"Ahmed Bouajjani","year":"2015","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: Rajamani, S.K., et al. (eds.) POPL 2015, pp. 651\u2013662. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-28869-2_5","volume-title":"Programming Languages and Systems","author":"S Burckhardt","year":"2012","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 87\u2013107. Springer, Heidelberg (2012)"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-33651-5_3","volume-title":"Distributed Computing","author":"A Gotsman","year":"2012","unstructured":"Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31\u201345. Springer, Heidelberg (2012)"},{"issue":"3","key":"33_CR9","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"9","key":"33_CR10","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess program. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Palsberg, J., Abadi, M. (eds.) POPL 2005, pp. 378\u2013391. ACM (2005)","DOI":"10.1145\/1047659.1040336"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"33_CR13","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.) PLDI 2011, pp. 175\u2013186. ACM (2011)","DOI":"10.1145\/1993316.1993520"},{"issue":"5","key":"33_CR14","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0020-0190(01)00337-4","volume":"83","author":"P Schnoebelen","year":"2002","unstructured":"Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5), 251\u2013261 (2002)","journal-title":"Inf. Process. Lett."},{"key":"33_CR15","unstructured":"Wang, C., Lv, Y., Wu, P.: Bounded TSO-to-SC linearizability is decidable. Technical report ISCAS-SKLCS-15-11, State Key Laboratory of Computer Science, ISCAS, CAS (2015). http:\/\/lcs.ios.ac.cn\/~lvyi\/files\/ISCAS-SKLCS-15-11.pdf"},{"key":"33_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-24953-7_24","volume-title":"Automated Technology for Verification and Analysis","author":"C Wang","year":"2015","unstructured":"Wang, C., Lv, Y., Wu, P.: TSO-to-TSO Linearizability Is Undecidable. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 309\u2013325. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2016: Theory and Practice of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49192-8_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T02:19:16Z","timestamp":1748744356000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49192-8_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662491911","9783662491928"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49192-8_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}