{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:57:10Z","timestamp":1760043430637,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662476659"},{"type":"electronic","value":"9783662476666"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-662-47666-6_8","type":"book-chapter","created":{"date-parts":[[2015,6,19]],"date-time":"2015-06-19T07:46:47Z","timestamp":1434700007000},"page":"95-107","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["On Reducing Linearizability to State Reachability"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Emmi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jad","family":"Hamza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,20]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/978-3-642-36742-7_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 324\u2013338. Springer, Heidelberg (2013)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., McMillan, K.L., Peled, D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1\u20132) (2000)","DOI":"10.1006\/inco.1999.2847"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"8_CR4","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: POPL 2015. ACM (2015)","DOI":"10.1145\/2676726.2677002"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: On reducing linearizability to state reachability. CoRR, abs\/1502.06882 (2015). arxiv.org\/abs\/1502.06882","DOI":"10.1007\/978-3-662-47666-6_8"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Dodds, M., Haas, A., Kirsch, C.M.: A scalable, correct time-stamped stack. In: POPL 2015. ACM (2015)","DOI":"10.1145\/2676726.2676963"},{"key":"8_CR7","series-title":"Lectures on Petri Nets I: Basic Models","volume-title":"Decidability and complexity of petri net problems\u2014an introduction","author":"J Esparza","year":"1998","unstructured":"Esparza, J.: Decidability and complexity of petri net problems\u2014an introduction. Lectures on Petri Nets I: Basic Models. Springer, Heidelberg (1998)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Filipovic, I., O\u2019Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51\u201352) (2010)","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4) (1997)","DOI":"10.1137\/S0097539794279614"},{"key":"8_CR10","unstructured":"Hamza, J.: On the complexity of linearizability. CoRR, abs\/1410.5000 (2014). arxiv.org\/abs\/1410.5000"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/978-3-642-40184-8_18","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"TA Henzinger","year":"2013","unstructured":"Henzinger, T.A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. LNCS, vol. 8052, pp. 242\u2013256. Springer, Heidelberg (2013)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3) (1990)","DOI":"10.1145\/78969.78972"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450\u2013464. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-47666-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T02:07:28Z","timestamp":1676945248000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-47666-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662476659","9783662476666"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-47666-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"20 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}