{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T20:36:15Z","timestamp":1794429375964,"version":"4.9.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642329395","type":"print"},{"value":"9783642329401","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32940-1_36","type":"book-chapter","created":{"date-parts":[[2012,9,1]],"date-time":"2012-09-01T16:47:02Z","timestamp":1346518022000},"page":"516-530","source":"Crossref","is-referenced-by-count":13,"title":["A Framework for Formally Verifying Software Transactional Memory Algorithms"],"prefix":"10.1007","author":[{"given":"Mohsen","family":"Lesani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor","family":"Luchangco","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark","family":"Moir","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"36_CR1","doi-asserted-by":"crossref","unstructured":"Cohen, A., O\u2019Leary, J., Pnueli, A., Tuttle, M., Zuck, L.: Verifying correctness of transactional memories. In: FMCAD 2007: Proceedings of Formal Methods in Computer Aided Design, pp. 37\u201344 (2007)","DOI":"10.1109\/FAMCAD.2007.40"},{"key":"36_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-70545-1_13","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2008","unstructured":"Cohen, A., Pnueli, A., Zuck, L.D.: Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 121\u2013134. Springer, Heidelberg (2008)"},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"Dalessandro, L., Spear, M., Scott, M.: NOrec: Streamlining STM by abolishing ownership records. In: PPoPP 2010: Proceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (January 2010)","DOI":"10.1145\/1693453.1693464"},{"key":"36_CR4","doi-asserted-by":"crossref","unstructured":"Dice, D., Shalev, O., Shavit, N.: Transactional locking II. In: International Symposium on Distributed Computing, pp. 194\u2013208 (2006)","DOI":"10.1007\/11864219_14"},{"key":"36_CR5","doi-asserted-by":"crossref","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Aspects of Computing (2012), \n                    \n                      http:\/\/labs.oracle.com\/projects\/scalable\/pubs\/Doherty-FAC-2012.pdf","DOI":"10.1007\/s00165-012-0225-8"},{"key":"36_CR6","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/1806596.1806613","volume-title":"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010","author":"M. Emmi","year":"2010","unstructured":"Emmi, M., Majumdar, R., Manevich, R.: Parameterized verification of transactional memories. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, pp. 134\u2013145. ACM, New York (2010)"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Henzinger, T., Jobstmann, B., Singh, V.: Model checking transactional memories. In: PLDI 2008: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 372\u2013382 (2008)","DOI":"10.1145\/1375581.1375626"},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: PPoPP 2008: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 175\u2013184 (2008)","DOI":"10.1145\/1345206.1345233"},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Moss, J.E.B.: Transactional memory: Architectural support for lock-free data structures. In: Proceedings of the 20th Annual International Symposium on Computer Architecture (1993)","DOI":"10.1145\/165123.165164"},{"key":"36_CR10","unstructured":"Lesani, M., Luchangco, V., Moir, M.: Putting opacity in its place (May 2012), \n                    \n                      http:\/\/labs.oracle.com\/projects\/scalable\/pubs\/OpacityInPlace.pdf"},{"key":"36_CR11","doi-asserted-by":"crossref","unstructured":"Lynch, N., Tuttle, M.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pp. 137\u2013151 (August 1987)","DOI":"10.1145\/41840.41852"},{"issue":"2","key":"36_CR12","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N. Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations, I: Untimed systems. Information and Computation\u00a0121(2), 214\u2013233 (1995)","journal-title":"Information and Computation"},{"issue":"2","key":"36_CR13","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2005.01.005","volume":"125","author":"S. Mitra","year":"2005","unstructured":"Mitra, S., Archer, M.: PVS strategies for proving abstraction properties of automata. Electron. Notes Theor. Comput. Sci.\u00a0125(2), 45\u201365 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"36_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Shankar, N., Rushby, J.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"36_CR15","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"C. Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.: The serializability of concurrent database updates. J. ACM\u00a026, 631\u2013653 (1979)","journal-title":"J. ACM"},{"key":"36_CR16","unstructured":"The PVS Specification and Verification System, \n                    \n                      http:\/\/pvs.csl.sri.com\/"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2012 \u2013 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32940-1_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:13:36Z","timestamp":1558300416000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32940-1_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642329395","9783642329401"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32940-1_36","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-32940-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}