{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T11:58:52Z","timestamp":1763726332941},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642119569"},{"type":"electronic","value":"9783642119576"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_13","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:55:38Z","timestamp":1268009738000},"page":"226-245","source":"Crossref","is-referenced-by-count":16,"title":["Logical Concurrency Control from Sequential Proofs"],"prefix":"10.1007","author":[{"given":"Jyotirmoy","family":"Deshmukh","sequence":"first","affiliation":[]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[]},{"given":"Venkatesh-Prasad","family":"Ranganath","sequence":"additional","affiliation":[]},{"given":"Kapil","family":"Vaswani","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"WYPIWYG examples (June 2009), http:\/\/research.microsoft.com\/en-us\/projects\/wypiwyg\/wypiwyg_examples.zip"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Cherem, S., Chilimbi, T., Gulwani, S.: Inferring locks for atomic sections. In: Proc. of PLDI (2008)","DOI":"10.1145\/1375581.1375619"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Deng, X., Dwyer, M.B., Hatcliff, J., Mizuno, M.: Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In: Proc. of ICSE, pp. 442\u2013452 (2002)","DOI":"10.1145\/581339.581394"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Deshmukh, J., Ramalingam, G., Ranganath, V.P., Vaswani, K.: Logical concurrency control from sequential proofs. Tech. Rep. MSR-TR-2009-81, Microsoft Research (2009)","DOI":"10.1007\/978-3-642-11957-6_13"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Elmas, T., Tasiran, S., Qadeer, S.: A calculus of atomic sections. In: Proc. of POPL (2009)","DOI":"10.1145\/1594834.1480885"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Emmi, M., Fischer, J., Jhala, R., Majumdar, R.: Lock allocation. In: Proc. of POPL (2007)","DOI":"10.1145\/1190216.1190260"},{"key":"13_CR8","unstructured":"Flanagan, C., Freund, S.N.: Automatic synchronization correction. In: Proc. of SCOOL (2005)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: A new algorithm for property checking. In: Proc. of FSE (November 2006)","DOI":"10.1145\/1181775.1181790"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. of POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. of POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"issue":"3","key":"13_CR12","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. Proc. of ACM TOPLAS\u00a012(3), 463\u2013492 (1990)","journal-title":"Proc. of ACM TOPLAS"},{"key":"13_CR13","unstructured":"Hicks, M., Foster, J.S., Pratikakis, P.: Lock inference for atomic sections. In: First Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (2006)"},{"key":"13_CR14","unstructured":"Janjua, M.U., Mycroft, A.: Automatic correcting transformations for safety property violations. In: Proc. of Thread Verification, pp. 111\u2013116 (2006)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"McCloskey, B., Zhou, F., Gay, D., Brewer, E.A.: Autolocker: Synchronization inference for atomic sections. In: Proc. of POPL (2006)","DOI":"10.1145\/1111037.1111068"},{"issue":"1-3","key":"13_CR16","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci.\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. In: Proc. of CACM (1976)","DOI":"10.1145\/360051.360224"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: Proc. of PLDI, pp. 136\u2013148 (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Vaziri, M., Tip, F., Dolby, J.: Associating synchronization constraints with data in an object-oriented language. In: Proc. of POPL, pp. 334\u2013345 (2006)","DOI":"10.1145\/1111037.1111067"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: Proc. of PLDI, pp. 125\u2013135 (2008)","DOI":"10.1145\/1375581.1375598"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/978-3-642-00768-2_13","volume-title":"TACAS 2009","author":"M. Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 139\u2013154. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11957-6_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:45:41Z","timestamp":1606185941000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}