{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T04:53:03Z","timestamp":1726030383141},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030206512"},{"type":"electronic","value":"9783030206529"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-20652-9_18","type":"book-chapter","created":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T23:03:25Z","timestamp":1558998205000},"page":"263-279","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Data Independence for Software Transactional Memory"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"K\u00f6nig","sequence":"first","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,5,28]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Dwarkadas, S., Rezine, A., Shriraman, A., Zhu, Y.: Verifying safety and liveness for the FlexTM hybrid transactional memory. In: DATE 2013, pp. 785\u2013790 (2013)","DOI":"10.7873\/DATE.2013.167"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. LNCS, vol. 7795, pp. 324\u2013338. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-36742-7_23"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Baek, W., Bronson, N.G., Kozyrakis, C., Olukotun, K.: Implementing and evaluating a model checker for transactional memory systems. In: ICECCS 2010, pp. 117\u2013126 (2010)","DOI":"10.1109\/ICECCS.2010.30"},{"issue":"1","key":"18_CR4","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/3093333.3009888","volume":"52","author":"A Bouajjani","year":"2017","unstructured":"Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. SIGPLAN Not. 52(1), 626\u2013638 (2017)","journal-title":"SIGPLAN Not."},{"key":"18_CR5","unstructured":"Bouajjani, A., Enea, C., Wang, C.: Checking linearizability of concurrent priority queues. In: CONCUR 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-15291-7_2","volume-title":"Euro-Par 2010 - Parallel Processing","author":"L Dalessandro","year":"2010","unstructured":"Dalessandro, L., Dice, D., Scott, M., Shavit, N., Spear, M.: Transactional mutex locks. In: D\u2019Ambra, P., Guarracino, M., Talia, D. (eds.) Euro-Par 2010. LNCS, vol. 6272, pp. 2\u201313. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-15291-7_2"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-319-19249-9_11","volume-title":"FM 2015: Formal Methods","author":"J Derrick","year":"2015","unstructured":"Derrick, J., Dongol, B., Schellhorn, G., Travkin, O., Wehrheim, H.: Verifying opacity of a transactional mutex lock. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 161\u2013177. Springer, Cham (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-319-19249-9_11"},{"key":"18_CR8","unstructured":"Doherty, S., Dongol, B., Derrick, J., Schellhorn, G., Wehrheim, H.: Proving opacity of a pessimistic STM. In: OPODIS 2016. LIPIcs, vol. 70, pp. 35:1\u201335:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)"},{"issue":"5","key":"18_CR9","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1007\/s00165-012-0225-8","volume":"25","author":"S Doherty","year":"2013","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Aspects Comput. 25(5), 769\u2013799 (2013)","journal-title":"Formal Aspects Comput."},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-85361-9_6","volume-title":"CONCUR 2008 - Concurrency Theory","author":"R Guerraoui","year":"2008","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Completeness and nondeterminism in model checking transactional memories. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 21\u201335. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-85361-9_6"},{"issue":"3","key":"18_CR11","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s00446-009-0092-6","volume":"22","author":"R Guerraoui","year":"2010","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Model checking transactional memories. Distrib. Comput. 22(3), 129\u2013145 (2010)","journal-title":"Distrib. Comput."},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2008, pp. 175\u2013184 (2008)","DOI":"10.1145\/1345206.1345233"},{"key":"18_CR13","series-title":"Synthesis Lectures on Distributed Computing Theory","volume-title":"The Theory of Timed I\/O Automata","author":"DK Kaynar","year":"2010","unstructured":"Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: The Theory of Timed I\/O Automata. Synthesis Lectures on Distributed Computing Theory, 2nd edn. Morgan & Claypool Publishers, San Rafael (2010)","edition":"2"},{"key":"18_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-67729-3_8","volume-title":"ICTAC 2017","author":"J K\u00f6nig","year":"2017","unstructured":"K\u00f6nig, J., Wehrheim, H.: Value-based or conflict-based? Opacity definitions for STMs. In: Hung, D., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580, pp. 118\u2013135. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-67729-3_8"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-662-45174-8_27","volume-title":"Distributed Computing","author":"M Lesani","year":"2014","unstructured":"Lesani, M., Palsberg, J.: Decomposing opacity. In: Kuhn, F. (ed.) DISC 2014. LNCS, vol. 8784, pp. 391\u2013405. Springer, Heidelberg (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-662-45174-8_27"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Shacham, O., et al.: Verifying atomicity via data independence. In: Proceedings of the 2014 International Symposium on Software Testing and Analysis, pp. 26\u201336. ACM (2014)","DOI":"10.1145\/2610384.2610402"},{"issue":"2","key":"18_CR17","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s004460050028","volume":"10","author":"N Shavit","year":"1997","unstructured":"Shavit, N., Touitou, D.: Software transactional memory. Distrib. Comput. 10(2), 99\u2013116 (1997)","journal-title":"Distrib. Comput."},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-319-51963-0_15","volume-title":"SOFSEM 2017: Theory and Practice of Computer Science","author":"C Wang","year":"2017","unstructured":"Wang, C., Lv, Y., Wu, P.: Decomposable relaxation for concurrent data structures. In: Steffen, B., Baier, C., van den Brand, M., Eder, J., Hinchey, M., Margaria, T. (eds.) SOFSEM 2017. LNCS, vol. 10139, pp. 188\u2013202. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-51963-0_15"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: POPL, pp. 184\u2013193 (1986)","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-20652-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T23:18:46Z","timestamp":1558999126000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-20652-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030206512","9783030206529"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-20652-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 May 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/robonaut.jsc.nasa.gov\/R2\/pages\/nfm2019.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}