{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T08:10:01Z","timestamp":1749888601909,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522333"},{"type":"electronic","value":"9783319522340"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_11","type":"book-chapter","created":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T04:52:06Z","timestamp":1484110326000},"page":"187-208","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Using Abstract Interpretation to Correct Synchronization Faults"],"prefix":"10.1007","author":[{"given":"Pietro","family":"Ferrara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Omer","family":"Tripp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peng","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Beeri, C., Bernstein, P.A., Goodman, N., Lai, M.Y., Shasha, D.E.: A concurrency control theory for nested transactions (preliminary report). In: Proceedings of the 2nd Annual ACM Symposium on Principles of Distributed Computing (PODC 1983), pp. 45\u201362. ACM Press, New York (1983)","key":"11_CR1","DOI":"10.1145\/800221.806709"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-19718-5_7","volume-title":"Programming Languages and Systems","author":"S Burckhardt","year":"2011","unstructured":"Burckhardt, S., Leijen, D.: Semantics of concurrent revisions. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 116\u2013135. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19718-5_7"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977. ACM Press (1977)","key":"11_CR3","DOI":"10.1145\/512950.512973"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Program. 13, 103\u2013179 (1992)","journal-title":"J. Logic Program."},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"1302","DOI":"10.1007\/s11227-013-0884-0","volume":"65","author":"IP Egwutuoha","year":"2013","unstructured":"Egwutuoha, I.P., Levy, D., Selic, B., Chen, S.: A survey of fault tolerance mechanisms and checkpoint\/restart implementations for high performance computing systems. J. Supercomput. 65, 1302\u20131326 (2013)","journal-title":"J. Supercomput."},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-04355-0_12","volume-title":"Distributed Computing","author":"P Felber","year":"2009","unstructured":"Felber, P., Gramoli, V., Guerraoui, R.: Elastic transactions. In: Keidar, I. (ed.) DISC 2009. LNCS, vol. 5805, pp. 93\u2013107. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04355-0_12"},{"doi-asserted-by":"crossref","unstructured":"Golan-Gueta, G., Ramalingam, G., Sagiv, M., Yahav, E.: Concurrent libraries with foresight. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 263\u2013274 (2013)","key":"11_CR7","DOI":"10.1145\/2491956.2462172"},{"doi-asserted-by":"crossref","unstructured":"Golan-Gueta, G., Ramalingam, G., Sagiv, M., Yahav, E.: Concurrent libraries with foresight. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, 16\u201319 June 2013, pp. 263\u2013274 (2013)","key":"11_CR8","DOI":"10.1145\/2499370.2462172"},{"doi-asserted-by":"crossref","unstructured":"Hawkins, P., Aiken, A., Fisher, K., Rinard, M.C., Sagiv, M.: Concurrent data representation synthesis. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, Beijing, China, 11\u201316 June 2012, pp. 417\u2013428 (2012)","key":"11_CR9","DOI":"10.1145\/2345156.2254114"},{"doi-asserted-by":"crossref","unstructured":"Hendler, D., Incze, I., Shavit, N., Tzafrir, M.: Flat combining and the synchronization-parallelism tradeoff. In: SPAA 2010: Proceedings of the 22nd Annual ACM Symposium on Parallelism in Algorithms and Architectures, Thira, Santorini, Greece, 13\u201315 June 2010, pp. 355\u2013364 (2010)","key":"11_CR10","DOI":"10.1145\/1810479.1810540"},{"doi-asserted-by":"crossref","unstructured":"Herlihy, M., Koskinen, E.: Transactional boosting: a methodology for highly-concurrent transactional objects. In: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2008, Salt Lake City, UT, USA, 20\u201323 February 2008, pp. 207\u2013216 (2008)","key":"11_CR11","DOI":"10.1145\/1345206.1345237"},{"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, San Diego, CA, pp. 289\u2013300, May 1993","key":"11_CR12","DOI":"10.1145\/173682.165164"},{"issue":"3","key":"11_CR13","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/2576793","volume":"57","author":"A Kleen","year":"2014","unstructured":"Kleen, A.: Scaling existing lock-based applications with lock elision. Commun. ACM 57(3), 52\u201356 (2014)","journal-title":"Commun. ACM"},{"doi-asserted-by":"crossref","unstructured":"Koskinen, E., Herlihy, M.: Checkpoints and continuations instead of nested transactions. In: Meyer auf der Heide, F., Shavit, N. (eds.) SPAA 2008: Proceedings of the 20th Annual ACM Symposium on Parallelism in Algorithms and Architectures, Munich, Germany, 14\u201316 June 2008, pp. 160\u2013168. ACM (2008)","key":"11_CR14","DOI":"10.1145\/1378533.1378563"},{"doi-asserted-by":"crossref","unstructured":"Koskinen, E., Parkinson, M.J.: The push\/pull model of transactions. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15\u201317 June 2015, pp. 186\u2013195 (2015)","key":"11_CR15","DOI":"10.1145\/2737924.2737995"},{"doi-asserted-by":"crossref","unstructured":"Kulkarni, M., Pingali, K., Walter, B., Ramanarayanan, G., Kavita Bala, L., Chew, P.: Optimistic parallelism requires abstractions. In: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2007, pp. 211\u2013222. ACM, New York (2007)","key":"11_CR16","DOI":"10.1145\/1250734.1250759"},{"doi-asserted-by":"crossref","unstructured":"Kulkarni, M., Pingali, K., Walter, B., Ramanarayanan, G., Kavita Bala, L., Chew, P.: Optimistic parallelism requires abstractions. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, 10\u201313 June 2007, pp. 211\u2013222 (2007)","key":"11_CR17","DOI":"10.1145\/1250734.1250759"},{"unstructured":"Matveev, A., Shavit, N.: Towards a fully pessimistic STM model. In: Proceedings of the Workshop on Transactional Memory (TRANSACT 2012) (2012)","key":"11_CR18"},{"doi-asserted-by":"crossref","unstructured":"McCloskey, B., Zhou, F., Gay, D., Brewer, E.A.: Autolocker: synchronization inference for atomic sections. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, 11\u201313 January 2006, pp. 346\u2013358 (2006)","key":"11_CR19","DOI":"10.1145\/1111320.1111068"},{"doi-asserted-by":"crossref","unstructured":"Ni, Y., Menon, V.S., Adl-Tabatabai, A.-R., Hosking, A.L., Hudson, R.L., Eliot, J., Moss, B., Saha, B., Shpeisman, T.: Open nesting in software transactional memory. In: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2007), pp. 68\u201378. ACM Press, New York (2007)","key":"11_CR20","DOI":"10.1145\/1229428.1229442"},{"doi-asserted-by":"crossref","unstructured":"Prountzos, D., Manevich, R., Pingali, K., McKinley, K.S.: A shape analysis for optimizing parallel graph programs. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 159\u2013172 (2011)","key":"11_CR21","DOI":"10.1145\/1926385.1926405"},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24, 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Shacham, O., Bronson, N.G., Aiken, A., Sagiv, M., Vechev, M.T., Yahav, E.: Testing atomicity of composed concurrent operations. In Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, Part of SPLASH 2011, Portland, OR, USA, 22\u201327 October 2011, pp. 51\u201364 (2011)","key":"11_CR23","DOI":"10.1145\/2048066.2048073"},{"doi-asserted-by":"crossref","unstructured":"Shacham, O., Yahav, E., Golan-Gueta, G., Aiken, A., Bronson, N.G., Sagiv, M., Vechev, M.T.: Verifying atomicity via data independence. In: International Symposium on Software Testing and Analysis, ISSTA 2014, San Jose, CA, USA, 21\u201326 July 2014, pp. 26\u201336 (2014)","key":"11_CR24","DOI":"10.1145\/2610384.2610402"},{"doi-asserted-by":"crossref","unstructured":"Tripp, O., Koskinen, E., Sagiv, M.: Turning nondeterminism into parallelism. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, Part of SPLASH 2013, Indianapolis, IN, USA, 26\u201331 October 2013, pp. 589\u2013604 (2013)","key":"11_CR25","DOI":"10.1145\/2544173.2509533"},{"doi-asserted-by":"crossref","unstructured":"Tripp, O., Yorsh, G., Field, J., Sagiv, M.: Hawkeye: effective discovery of dataflow impediments to parallelization. In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2011, pp. 207\u2013224. ACM, New York (2011)","key":"11_CR26","DOI":"10.1145\/2048066.2048085"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52234-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T07:43:24Z","timestamp":1749887004000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"12 January 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/conf.researchr.org\/home\/VMCAI-2017","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}