{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:12:40Z","timestamp":1759032760309},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,12,1]],"date-time":"2009-12-01T00:00:00Z","timestamp":1259625600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Distrib. Comput."],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1007\/s00446-009-0092-6","type":"journal-article","created":{"date-parts":[[2009,11,30]],"date-time":"2009-11-30T10:09:42Z","timestamp":1259575782000},"page":"129-145","source":"Crossref","is-referenced-by-count":18,"title":["Model checking transactional memories"],"prefix":"10.1007","volume":"22","author":[{"given":"Rachid","family":"Guerraoui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vasu","family":"Singh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,12,1]]},"reference":[{"key":"92_CR1","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1006\/inco.1999.2847","volume":"160","author":"R. Alur","year":"2000","unstructured":"Alur R., McMillan K.L., Peled D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160, 167\u2013188 (2000)","journal-title":"Inf. Comput."},{"key":"92_CR2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/s00446-003-0088-6","volume":"16","author":"J.H. Anderson","year":"2003","unstructured":"Anderson J.H., Kim Y., Herman T.: Shared-memory mutual exclusion: major research trends since 1986. Distrib. Comput. 16, 75\u2013110 (2003)","journal-title":"Distrib. Comput."},{"issue":"11","key":"92_CR3","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"Browne M.C., Clarke E.M., Grumberg O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(11), 13\u201331 (1989)","journal-title":"Inf. Comput."},{"key":"92_CR4","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp. 12\u201321 (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"92_CR5","doi-asserted-by":"crossref","unstructured":"Cohen, A., O\u2019Leary, J., Pnueli, A., Tuttle, M.R., Zuck, L.: Verifying correctness of transactional memories. In: FMCAD, pp. 37\u201344 (2007)","DOI":"10.1109\/FAMCAD.2007.40"},{"key":"92_CR6","doi-asserted-by":"crossref","unstructured":"Cohen, A., Pnueli, A., Zuck, L.D.: Mechanical verification of transactional memories with non-transactional memory accesses. In: CAV, pp. 121\u2013134. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_13"},{"key":"92_CR7","doi-asserted-by":"crossref","unstructured":"Dice, D., Shalev, O., Shavit, N.: Transactional locking II. In: DISC, pp. 194\u2013208. Springer (2006)","DOI":"10.1007\/11864219_14"},{"issue":"11","key":"92_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(85)90206-3","volume":"38","author":"M. Fl\u00e9","year":"1985","unstructured":"Fl\u00e9 M., Roucairol G.: Maximal serializability of iterated transactions. Theor. Comput. Sci. 38(11), 1\u201316 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"92_CR9","doi-asserted-by":"crossref","unstructured":"Fraser, K., Harris, T.: Concurrent programming without locks. ACM Trans. Comput. Syst. (2007)","DOI":"10.1145\/1233307.1233309"},{"key":"92_CR10","doi-asserted-by":"crossref","unstructured":"Gopalakrishnan, G., Yang, Y., Sivaraj, H.: QB or Not QB: an efficient execution verification tool for memory orderings. In: CAV, pp. 401\u2013413. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_31"},{"key":"92_CR11","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Henzinger, T.A., Jobstmann, B., Singh, V.: Model checking transactional memories. In: PLDI, pp. 372\u2013382 (2008)","DOI":"10.1145\/1375581.1375626"},{"key":"92_CR12","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Completeness and nondeterminism in model checking transactional memories. In: CONCUR, pp. 21\u201335 (2008)","DOI":"10.1007\/978-3-540-85361-9_6"},{"key":"92_CR13","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Software transactional memory on relaxed memory models. In: CAV, pp. 321\u2013336 (2009)","DOI":"10.1007\/978-3-642-02658-4_26"},{"key":"92_CR14","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Herlihy, M., Pochon, B.: Polymorphic contention management. In: DISC, pp. 303\u2013323 (2005)","DOI":"10.1007\/11561927_23"},{"key":"92_CR15","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: PPoPP, pp. 175\u2013184 (2008)","DOI":"10.1145\/1345206.1345233"},{"key":"92_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Verifying sequential consistency on shared-memory multiprocessor systems. In CAV, pp. 301\u2013315. Springer (1999)","DOI":"10.1007\/3-540-48683-6_27"},{"issue":"1","key":"92_CR17","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1145\/114005.102808","volume":"13","author":"M. Herlihy","year":"1991","unstructured":"Herlihy M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1), 124\u2013149 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"92_CR18","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Luchangco, V., Moir, M.: Obstruction-free synchronization: double-ended queues as an example. In: ICDCS, pp. 522\u2013529. IEEE Computer Society (2003)","DOI":"10.1109\/ICDCS.2003.1203503"},{"key":"92_CR19","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Luchangco, V., Moir, M., Scherer, W.N.: Software transactional memory for dynamic-sized data structures. In: PODC, pp. 92\u2013101 (2003)","DOI":"10.1145\/872035.872048"},{"key":"92_CR20","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Moss, J.E.B.: Transactional memory: architectural support for lock-free data structures. In: ISCA, pp. 289\u2013300. ACM Press (1993)","DOI":"10.1145\/165123.165164"},{"key":"92_CR21","doi-asserted-by":"crossref","unstructured":"Larus, J.R., Rajwar, R.: Transactional Memory. Synthesis Lectures on Computer Architecture. Morgan & Claypool (2007)","DOI":"10.2200\/S00070ED1V01Y200611CAC002"},{"issue":"4","key":"92_CR22","doi-asserted-by":"crossref","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"C.H. Papadimitriou","year":"1979","unstructured":"Papadimitriou C.H.: The serializability of concurrent database updates. J. ACM 26(4), 631\u2013653 (1979)","journal-title":"J. ACM"},{"key":"92_CR23","doi-asserted-by":"crossref","unstructured":"Qadeer, S.: Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Transactions on Parallel and Distributed Systems, 730\u2013741 (2003)","DOI":"10.1109\/TPDS.2003.1225053"},{"key":"92_CR24","doi-asserted-by":"crossref","unstructured":"Scherer, W.N., Scott, M.L.: Advanced contention management for dynamic software transactional memory. In: PODC, pp. 240\u2013248 (2005)","DOI":"10.1145\/1073814.1073861"},{"key":"92_CR25","unstructured":"Scott, M.L.: Sequential specification of transactional memory semantics. In: TRANSACT (2006)"},{"key":"92_CR26","doi-asserted-by":"crossref","unstructured":"Shavit, N., Touitou, D.: Software transactional memory. In: PODC, pp. 204\u2013213 (1995)","DOI":"10.1145\/224964.224987"},{"key":"92_CR27","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R.S. Streett","year":"1982","unstructured":"Streett R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Inf. Control 54, 121\u2013141 (1982)","journal-title":"Inf. Control"},{"key":"92_CR28","doi-asserted-by":"crossref","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: CAV, pp. 17\u201330. Springer (2006)","DOI":"10.1007\/11817963_5"}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-009-0092-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00446-009-0092-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-009-0092-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T09:26:43Z","timestamp":1559122003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00446-009-0092-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,12,1]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["92"],"URL":"https:\/\/doi.org\/10.1007\/s00446-009-0092-6","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"value":"0178-2770","type":"print"},{"value":"1432-0452","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,12,1]]}}}