{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:23:31Z","timestamp":1725791011065},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548321"},{"type":"electronic","value":"9783642548338"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54833-8_17","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T05:37:17Z","timestamp":1395380237000},"page":"311-330","source":"Crossref","is-referenced-by-count":2,"title":["Checking Linearizability of Encapsulated Extended Operations"],"prefix":"10.1007","author":[{"given":"Oren","family":"Zomer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guy","family":"Golan-Gueta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","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: OOPSLA, pp. 51\u201364 (2011)","DOI":"10.1145\/2076021.2048073"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. TOPLAS\u00a012(3) (1990)","DOI":"10.1145\/78969.78972"},{"issue":"1-2","key":"17_CR3","doi-asserted-by":"publisher","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.\u00a0160(1-2), 167\u2013188 (2000)","journal-title":"Inf. Comput."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Zomer, O., Golan-Gueta, G., Ramalingam, G., Sagiv, M.: Checking linearizability of encapsulated extended operations. Technical report, Tel Aviv University (2013), http:\/\/www.cs.tau.ac.il\/~ggolan\/papers\/ESOP14TechRep.pdf","DOI":"10.1007\/978-3-642-54833-8_17"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Shacham, O.: Verifying Atomicity of Composed Concurrent Operations. PhD thesis, Tel Aviv University (2012)","DOI":"10.1145\/2048066.2048073"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Golan-Gueta, G., Ramalingam, G., Sagiv, M., Yahav, E.: Concurrent libraries with foresight. In: PLDI, pp. 263\u2013274 (2013)","DOI":"10.1145\/2499370.2462172"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Towards a theory of parallel programming. Operating System Techniques (1972)","DOI":"10.1007\/978-1-4757-3472-0_6"},{"key":"17_CR8","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress (1983)"},{"issue":"3","key":"17_CR9","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/357103.357109","volume":"2","author":"E. Clarke Jr.","year":"1980","unstructured":"Clarke Jr., E.: Synthesis of resource invariants for concurrent programs. TOPLAS\u00a02(3), 338\u2013358 (1980)","journal-title":"TOPLAS"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"17_CR11","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1145\/1250734.1250765","volume-title":"Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2007","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2007, pp. 266\u2013277. ACM, New York (2007)"},{"issue":"51-52","key":"17_CR12","doi-asserted-by":"publisher","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"I. Filipovic","year":"2010","unstructured":"Filipovic, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theoretical Computer Science\u00a0411(51-52), 4379\u20134398 (2010)","journal-title":"Theoretical Computer Science"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-642-12002-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2010","unstructured":"Ball, T., Burckhardt, S., Coons, K.E., Musuvathi, M., Qadeer, S.: Preemption sealing for efficient concurrency testing. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 420\u2013434. Springer, Heidelberg (2010)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338\u2013349 (2003)","DOI":"10.1145\/780822.781169"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, pp. 446\u2013455 (2007)","DOI":"10.1145\/1273442.1250785"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL, pp. 2\u201315 (2009)","DOI":"10.1145\/1594834.1480885"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Elmas, T., Tasiran, S., Qadeer, S.: Vyrd: verifying concurrent programs by runtime refinement-violation detection. In: PLDI, pp. 27\u201337 (2005)","DOI":"10.1145\/1064978.1065015"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: PLDI, pp. 330\u2013340 (2010)","DOI":"10.1145\/1809028.1806634"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP (2006)","DOI":"10.1145\/1122971.1122992"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"S. Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol.\u00a03235, pp. 97\u2013114. Springer, Heidelberg (2004)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/11817963_44","volume-title":"Computer Aided Verification","author":"R. Colvin","year":"2006","unstructured":"Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set algorithm. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 475\u2013488. Springer, Heidelberg (2006)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-27813-9_4","volume-title":"Computer Aided Verification","author":"H. Gao","year":"2004","unstructured":"Gao, H., Hesselink, W.H.: A formal reduction for lock-free parallel algorithms. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 44\u201356. Springer, Heidelberg (2004)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-73368-3_49","volume-title":"Computer Aided Verification","author":"D. Amit","year":"2007","unstructured":"Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 477\u2013490. Springer, Heidelberg (2007)"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-540-70545-1_37","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2008","unstructured":"Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread quantification for concurrent shape analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 399\u2013413. Springer, Heidelberg (2008)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-69166-2_24","volume-title":"Static Analysis","author":"R. Manevich","year":"2008","unstructured":"Manevich, R., Lev-Ami, T., Sagiv, M., Ramalingam, G., Berdine, J.: Heap decomposition for concurrent shape analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 363\u2013377. Springer, Heidelberg (2008)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V. Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 450\u2013464. Springer, Heidelberg (2010)"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Turon, A.: Reagents: expressing and composing fine-grained concurrency. In: PLDI, pp. 157\u2013168 (2012)","DOI":"10.1145\/2345156.2254084"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Hawkins, P., Aiken, A., Fisher, K., Rinard, M.C., Sagiv, M.: Concurrent data representation synthesis. In: PLDI, pp. 417\u2013428 (2012)","DOI":"10.1145\/2345156.2254114"}],"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-54833-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,16]],"date-time":"2020-08-16T12:27:37Z","timestamp":1597580857000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54833-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548321","9783642548338"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54833-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}