{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:51:41Z","timestamp":1743069101236,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319147192"},{"type":"electronic","value":"9783319147208"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-14720-8_14","type":"book-chapter","created":{"date-parts":[[2014,12,29]],"date-time":"2014-12-29T09:26:01Z","timestamp":1419845161000},"page":"283-306","source":"Crossref","is-referenced-by-count":1,"title":["Verification Tools for Transactional Programs"],"prefix":"10.1007","author":[{"given":"Adrian","family":"Cristal","sequence":"first","affiliation":[]},{"given":"Burcu Kulahcioglu","family":"Ozkan","sequence":"additional","affiliation":[]},{"given":"Ernie","family":"Cohen","sequence":"additional","affiliation":[]},{"given":"Gokcen","family":"Kestor","sequence":"additional","affiliation":[]},{"given":"Ismail","family":"Kuru","sequence":"additional","affiliation":[]},{"given":"Osman","family":"Unsal","sequence":"additional","affiliation":[]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[]},{"given":"Suha Orhun","family":"Mutluergil","sequence":"additional","affiliation":[]},{"given":"Tayfun","family":"Elmas","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/1328897.1328449","volume":"43","author":"M. Abadi","year":"2008","unstructured":"Abadi, M., Birrell, A., Harris, T., Isard, M.: Semantics of transactional memory and automatic mutual exclusion. SIGPLAN Not.\u00a043(1), 63\u201374 (2008)","journal-title":"SIGPLAN Not."},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-540-85361-9_5","volume-title":"CONCUR 2008 - Concurrency Theory","author":"M. Abadi","year":"2008","unstructured":"Abadi, M., Harris, T., Moore, K.F.: A model of dynamic separation for transactional memory. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol.\u00a05201, pp. 6\u201320. Springer, Heidelberg (2008)"},{"key":"14_CR3","unstructured":"Adya, A.: Weak consistency: a generalized theory and optimistic implementations for distributed transactions. PhD thesis, AAI0800775 (1999)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-642-37036-6_28","volume-title":"Programming Languages and Systems","author":"J. Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software Verification for Weak Memory via Program Transformation. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. LNCS, vol.\u00a07792, pp. 512\u2013532. Springer, Heidelberg (2013)"},{"key":"14_CR5","first-page":"341","volume-title":"Proceedings of the 2009 IEEE International Conference on Data Engineering, ICDE 2009","author":"M. Alomari","year":"2009","unstructured":"Alomari, M., Fekete, A., R\u00f6hm, U.: A robust technique to ensure serializable executions with snapshot isolation dbms. In: Proceedings of the 2009 IEEE International Conference on Data Engineering, ICDE 2009, pp. 341\u2013352. IEEE Computer Society, Washington, DC (2009)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"M.F. Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 99\u2013115. Springer, Heidelberg (2011)"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/1707801.1706305","volume":"45","author":"H. Attiya","year":"2010","unstructured":"Attiya, H., Ramalingam, G., Rinetzky, N.: Sequential verification of serializability. SIGPLAN Not\u00a045, 31\u201342 (2010)","journal-title":"SIGPLAN Not"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"14_CR9","doi-asserted-by":"publisher","first-page":"729","DOI":"10.1145\/1376616.1376690","volume-title":"Proceedings of the 2008 ACM SIGMOD International Conference on Management of Data, SIGMOD 2008","author":"M.J. Cahill","year":"2008","unstructured":"Cahill, M.J., R\u00f6hm, U., Fekete, A.D.: Serializable isolation for snapshot databases. In: Proceedings of the 2008 ACM SIGMOD International Conference on Management of Data, SIGMOD 2008, pp. 729\u2013738. ACM, New York (2008)"},{"key":"14_CR10","unstructured":"Minh, C.C., Chung, J.W., Kozyrakis, C., Olukotun, K.: STAMP: Stanford transactional applications for multi-processing. In: Proc. of the IEEE International Symposium on Workload Characterization, IISWC 2008 (September 2008)"},{"issue":"2","key":"14_CR11","doi-asserted-by":"publisher","first-page":"1277","DOI":"10.14778\/1454159.1454167","volume":"1","author":"B.F. Cooper","year":"2008","unstructured":"Cooper, B.F., Ramakrishnan, R., Srivastava, U., Silberstein, A., Bohannon, P., Jacobsen, H.-A., Puz, N., Weaver, D., Yerneni, R.: Pnuts: Yahoo!\u2019s hosted data serving platform. Proceedings of the VLDB Endowment\u00a01(2), 1277\u20131288 (2008)","journal-title":"Proceedings of the VLDB Endowment"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: Vcc: Contract-based modular verification of concurrent c. In: ICSE-Companion 2009, pp. 429\u2013430 (May 2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-15763-9_4","volume-title":"Distributed Computing","author":"L. Dalessandro","year":"2010","unstructured":"Dalessandro, L., Scott, M.L., Spear, M.F.: Transactions as the Foundation of a Memory Consistency Model. In: Lynch, N.A., Shvartsman, A.A. (eds.) DISC 2010. LNCS, vol.\u00a06343, pp. 20\u201334. Springer, Heidelberg (2010)"},{"key":"14_CR14","unstructured":"Daudjee, K., Salem, K.: Lazy database replication with snapshot isolation. In: Proceedings of the 32nd International Conference on Very Large Data Bases, pp. 715\u2013726. VLDB Endowment (2006)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-31057-7_28","volume-title":"ECOOP 2012 \u2013 Object-Oriented Programming","author":"R.J. Dias","year":"2012","unstructured":"Dias, R.J., Distefano, D., Seco, J.C., Louren\u00e7o, J.M.: Verification of Snapshot Isolation in Transactional Memory Java Programs. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol.\u00a07313, pp. 640\u2013664. Springer, Heidelberg (2012)"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/1250734.1250762","volume-title":"PLDI 2007: Proc. of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"T. Elmas","year":"2007","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: a race and transaction-aware java runtime. In: PLDI 2007: Proc. of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 245\u2013255. ACM, New York (2007)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-15769-1_2","volume-title":"Static Analysis","author":"M. F\u00e4hndrich","year":"2010","unstructured":"F\u00e4hndrich, M.: Static Verification for Code Contracts. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 2\u20135. Springer, Heidelberg (2010)"},{"issue":"2","key":"14_CR18","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1145\/1071610.1071615","volume":"30","author":"A. Fekete","year":"2005","unstructured":"Fekete, A., Liarokapis, D., O\u2019Neil, E., O\u2019Neil, P., Shasha, D.: Making snapshot isolation serializable. ACM Transactions on Database Systems (TODS)\u00a030(2), 492\u2013528 (2005)","journal-title":"ACM Transactions on Database Systems (TODS)"},{"key":"14_CR19","first-page":"234","volume-title":"PLDI 2002","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI 2002, pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/1178597.1178609","volume-title":"MSPC 2006: Proc. of the 2006 Workshop on Memory System Performance and Correctness","author":"D. Grossman","year":"2006","unstructured":"Grossman, D., Manson, J., Pugh, W.: What do high-level memory models mean for transactions? In: MSPC 2006: Proc. of the 2006 Workshop on Memory System Performance and Correctness, pp. 62\u201369. ACM Press, New York (2006)"},{"key":"14_CR21","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/1178597.1178609","volume-title":"Proceedings of the 2006 Workshop on Memory System Performance and Correctness, MSPC 2006","author":"D. Grossman","year":"2006","unstructured":"Grossman, D., Manson, J., Pugh, W.: What do high-level memory models mean for transactions? In: Proceedings of the 2006 Workshop on Memory System Performance and Correctness, MSPC 2006, pp. 62\u201369. ACM, New York (2006)"},{"key":"14_CR22","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1145\/949305.949340","volume-title":"OOPSLA 2003: Proc. of the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programing, Systems, Languages, and Applications","author":"T. Harris","year":"2003","unstructured":"Harris, T., Fraser, K.: Language support for lightweight transactions. In: OOPSLA 2003: Proc. of the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programing, Systems, Languages, and Applications, pp. 388\u2013402. ACM Press, New York (2003)"},{"key":"14_CR23","first-page":"48","volume-title":"PPoPP 2005: Proc. of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming","author":"T. Harris","year":"2005","unstructured":"Harris, T., Marlow, S., Peyton-Jones, S., Herlihy, M.: Composable memory transactions. In: PPoPP 2005: Proc. of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 48\u201360. ACM Press, New York (2005)"},{"key":"14_CR24","unstructured":"Herlihy, M.: SXM1.1: Software transactional memory package for c#. Tech. rep., Brown University & Microsoft Research (May 2005)"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Moss, J.E.B.: Transactional memory: Architectural support for lock-free data structures. In: Proc. of the Twentieth Annual International Symposium on Computer Architecture (1993)","DOI":"10.1145\/165123.165164"},{"issue":"3","key":"14_CR26","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M.P. Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst.\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR27","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1178597.1178611","volume-title":"Proceedings of the 2006 Workshop on Memory System Performance and Correctness, MSPC 2006","author":"B. Hindman","year":"2006","unstructured":"Hindman, B., Grossman, D.: Atomicity via source-to-source translation. In: Proceedings of the 2006 Workshop on Memory System Performance and Correctness, MSPC 2006, pp. 82\u201391. ACM, New York (2006)"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Kestor, G., Unsal, O.S., Cristal, A., Tasiran, S.: T-rex: A dynamic race detection tool for c\/c++ transactional memory applications. In: Proceedings of the Ninth European Conference on Computer Systems, EuroSys 2014, pp. 20:1\u201320:12. ACM, New York (2014)","DOI":"10.1145\/2592798.2592809"},{"key":"14_CR29","unstructured":"Kuru, I., Ozkan, B.K., Mutluergil, S.O., Tasiran, S., Elmas, T., Cohen, E.: Verifying programs under snapshot isolation and similar relaxed consistency models. In: Workshop on Transactional Computing, TRANSACT (2014)"},{"key":"14_CR30","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1145\/1378533.1378588","volume-title":"Proceedings of the Twentieth Annual Symposium on Parallelism in Algorithms and Architectures, SPAA 2008","author":"V. Menon","year":"2008","unstructured":"Menon, V., Balensiefer, S., Shpeisman, T., Adl-Tabatabai, A.-R., Hudson, R.L., Saha, B., Welc, A.: Practical weak-atomicity semantics for java stm. In: Proceedings of the Twentieth Annual Symposium on Parallelism in Algorithms and Architectures, SPAA 2008, pp. 314\u2013325. ACM, New York (2008)"},{"key":"14_CR31","unstructured":"Papadimitriou, C.: The theory of database concurrency control. Computer Science Press (1986)"},{"issue":"4","key":"14_CR32","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst.\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"4","key":"14_CR33","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst.\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"key":"14_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-16612-9_29","volume-title":"Runtime Verification","author":"A. Sezgin","year":"2010","unstructured":"Sezgin, A., Tasiran, S., Muslu, K., Qadeer, S.: Run-time verification of optimistic concurrency. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 384\u2013398. Springer, Heidelberg (2010)"},{"key":"14_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-642-15057-9_2","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A. Sezgin","year":"2010","unstructured":"Sezgin, A., Tasiran, S., Qadeer, S.: Tressa: Claiming the future. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 25\u201339. Springer, Heidelberg (2010)"},{"key":"14_CR36","unstructured":"Skare, T., Kozyrakis, C.: Early release: Friend or foe?. In: Workshop on Transactional Memory Workloads (June 2006)"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Sovran, Y., Power, R., Aguilera, M.K., Li, J.: Transactional storage for geo-replicated systems. In: Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, pp. 385\u2013400. ACM (2011)","DOI":"10.1145\/2043556.2043592"},{"issue":"5","key":"14_CR38","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/224057.224070","volume":"29","author":"D.B. Terry","year":"1995","unstructured":"Terry, D.B., Theimer, M.M., Petersen, K., Demers, A.J., Spreitzer, M.J., Hauser, C.H.: Managing update conflicts in bayou, a weakly connected replicated storage system. ACM SIGOPS Operating Systems Review\u00a029(5), 172\u2013182 (1995)","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"14_CR39","unstructured":"Titos, R., Acacio, M.E., Garc\u00eda, J.M., Harris, T., Cristal, A., Unsal, O., Valero, M.: Hardware transactional memory with software-defined conflicts. In: High-Performance and Embedded Architectures and Compilation (HiPEAC 2012) (January 2012)"}],"container-title":["Lecture Notes in Computer Science","Transactional Memory. Foundations, Algorithms, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-14720-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T22:22:14Z","timestamp":1559082134000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-14720-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319147192","9783319147208"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-14720-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}