{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:45:19Z","timestamp":1725727519833},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642391750"},{"type":"electronic","value":"9783642391767"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39176-7_20","type":"book-chapter","created":{"date-parts":[[2013,5,30]],"date-time":"2013-05-30T04:58:44Z","timestamp":1369889924000},"page":"320-340","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking Unbounded Concurrent Lists"],"prefix":"10.1007","author":[{"given":"Divjyot","family":"Sethi","sequence":"first","affiliation":[]},{"given":"Muralidhar","family":"Talupur","sequence":"additional","affiliation":[]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","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":"20_CR2","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1145\/1806596.1806634","volume-title":"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010","author":"S. Burckhardt","year":"2010","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, pp. 330\u2013340. ACM, New York (2010)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-74061-2_15","volume-title":"Static Analysis","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 233\u2013248. Springer, Heidelberg (2007)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-642-14295-6_41","volume-title":"Computer Aided Verification","author":"P. \u010cern\u00fd","year":"2010","unstructured":"\u010cern\u00fd, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 465\u2013479. Springer, Heidelberg (2010)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C.-T. Chou","year":"2004","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 382\u2013398. Springer, Heidelberg (2004)"},{"key":"20_CR6","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":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T. Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 504\u2013528. Springer, Heidelberg (2010)"},{"issue":"6","key":"20_CR8","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1145\/1273442.1250765","volume":"42","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. SIGPLAN Not.\u00a042(6), 266\u2013277 (2007)","journal-title":"SIGPLAN Not."},{"key":"20_CR9","volume-title":"The Art of Multiprocessor Programming","author":"M. Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco (2008)"},{"key":"20_CR10","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, 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR11","first-page":"271","volume-title":"Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011","author":"B. Jacobs","year":"2011","unstructured":"Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 271\u2013282. ACM, New York (2011)"},{"doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Bryant, R.E.: Predicate abstraction with indexed predicates. ACM Trans. Comput. Logic 9 (December 2007)","key":"20_CR12","DOI":"10.1145\/1297658.1297662"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-05089-3_21","volume-title":"FM 2009: Formal Methods","author":"Y. Liu","year":"2009","unstructured":"Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 321\u2013337. Springer, Heidelberg (2009)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 219\u2013237. Springer, Heidelberg (1999)"},{"unstructured":"Michael, M.M., Scott, M.L.: Correction of a memory management method for lock-free data structures. Tech. rep., Rochester, NY, USA (1995)","key":"20_CR15"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-68237-0_8","volume-title":"FM 2008: Formal Methods","author":"T. Noll","year":"2008","unstructured":"Noll, T., Rieger, S.: Verifying dynamic pointer-manipulating threads. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 84\u201399. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"O\u2019Leary, J., Talupur, M., Tuttle, M.: Protocol verification using flows: An industrial experience. In: Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 172\u2013179 (November 2009)","key":"20_CR17","DOI":"10.1109\/FMCAD.2009.5351126"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0,1,\u2009\u221e\u2009)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"20_CR20","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/292540.292552","volume-title":"Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999","author":"M. Sagiv","year":"1999","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999, pp. 105\u2013118. ACM, New York (1999)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-31759-0_15","volume-title":"Model Checking Software","author":"D. Sethi","year":"2012","unstructured":"Sethi, D., Talupur, M., Schwartz-Narbonne, D., Malik, S.: Parameterized model checking of fine grained concurrency. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol.\u00a07385, pp. 208\u2013226. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Talupur, M., Tuttle, M.: Going with the flow: Parameterized verification using message flows. In: Formal Methods in Computer-Aided Design, FMCAD 2008, pp. 1\u20138 (November 2008)","key":"20_CR22","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-540-93900-9_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. Vafeiadis","year":"2009","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 335\u2013348. Springer, Heidelberg (2009)"},{"key":"20_CR24","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":"20_CR25","first-page":"129","volume-title":"PPoPP 2006","author":"V. Vafeiadis","year":"2006","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP 2006, pp. 129\u2013136. ACM, New York (2006)"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-02652-2_21","volume-title":"Model Checking Software","author":"M. Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: P\u0103s\u0103reanu, C.S. (ed.) SPIN 2009. LNCS, vol.\u00a05578, pp. 261\u2013278. Springer, Heidelberg (2009)"},{"key":"20_CR27","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/360204.360206","volume-title":"Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001","author":"E. Yahav","year":"2001","unstructured":"Yahav, E.: Verifying safety properties of concurrent java programs using 3-valued logic. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001, pp. 27\u201340. ACM, New York (2001)"},{"key":"20_CR28","first-page":"1185","volume-title":"Proceeding of the 33rd International Conference on Software Engineering, ICSE 2011","author":"S.J. Zhang","year":"2011","unstructured":"Zhang, S.J.: Scalable automatic linearizability checking. In: Proceeding of the 33rd International Conference on Software Engineering, ICSE 2011, pp. 1185\u20131187. ACM, New York (2011)"},{"key":"20_CR29","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1109\/SSIRI.2010.37","volume-title":"Proceedings of the 2010 Fourth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2010","author":"S.J. Zhang","year":"2010","unstructured":"Zhang, S.J., Liu, Y.: Model checking a lazy concurrent list-based set algorithm. In: Proceedings of the 2010 Fourth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2010, pp. 43\u201352. IEEE Computer Society, Washington, DC (2010)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39176-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T08:56:33Z","timestamp":1557737793000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39176-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642391750","9783642391767"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39176-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}