{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T20:34:18Z","timestamp":1648845258073},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,2,15]],"date-time":"2015-02-15T00:00:00Z","timestamp":1423958400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,8]]},"DOI":"10.1007\/s10009-015-0369-y","type":"journal-article","created":{"date-parts":[[2015,2,17]],"date-time":"2015-02-17T09:56:52Z","timestamp":1424167012000},"page":"375-391","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model checking unbounded concurrent lists"],"prefix":"10.1007","volume":"18","author":[{"given":"Divjyot","family":"Sethi","sequence":"first","affiliation":[]},{"given":"Muralidhar","family":"Talupur","sequence":"additional","affiliation":[]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,2,15]]},"reference":[{"key":"369_CR1","doi-asserted-by":"crossref","unstructured":"Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread quantification for concurrent shape analysis. In: Proceedings of CAV \u201908, pp. 399\u2013413. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1_37"},{"key":"369_CR2","doi-asserted-by":"crossref","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 \u201910, pp. 330\u2013340. ACM, New York, NY, USA (2010)","DOI":"10.1145\/1806596.1806634"},{"key":"369_CR3","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Static Analysis, pp. 233\u2013248. Springer, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-74061-2_15"},{"key":"369_CR4","doi-asserted-by":"crossref","unstructured":"Cern\u00fd, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Proceedings of Computer Aided Verification, pp. 465\u2013479 (2010)","DOI":"10.1007\/978-3-642-14295-6_41"},{"key":"369_CR5","doi-asserted-by":"crossref","unstructured":"Chou, C.T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Proceedings of FMCAD (2004)","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"369_CR6","doi-asserted-by":"crossref","unstructured":"Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set algorithm. In: Computer Aided Verification, pp. 475\u2013488. Springer, Berlin, Heidelberg (2006)","DOI":"10.1007\/11817963_44"},{"key":"369_CR7","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Computer Aided Verification. pp. 160\u2013171. Springer, Berlin, Heidelberg (1999)","DOI":"10.1007\/3-540-48683-6_16"},{"key":"369_CR8","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: Proceedings of the 24th European Conference on Object-Oriented Programming. ECOOP\u201910, pp. 504\u2013528. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14107-2_24"},{"issue":"1\u20133","key":"369_CR9","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Progr. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Progr."},{"issue":"6","key":"369_CR10","doi-asserted-by":"crossref","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. 42(6), 266\u2013277 (2007)","journal-title":"SIGPLAN Not."},{"key":"369_CR11","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":"369_CR12","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"369_CR13","doi-asserted-by":"crossref","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 \u201911, pp. 271\u2013282. ACM, New York (2011)","DOI":"10.1145\/1926385.1926417"},{"key":"369_CR14","unstructured":"Kristic, S.: Parameterized system verification with guard strengthening and parameter abstraction. In: Proceedings of 4th International Workshop on Automatic Verification of Finite State Systems (2005)"},{"key":"369_CR15","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Bryant, R.E.: Predicate abstraction with indexed predicates. ACM Trans. Comput. Logic (TOCL) 9(1) (2007)","DOI":"10.1145\/1297658.1297662"},{"key":"369_CR16","doi-asserted-by":"crossref","unstructured":"Lea, D.: The java.util.concurrent synchronizer framework. Sci. Comput. Program. 58, 293\u2013309 (2005). http:\/\/dl.acm.org\/citation.cfm?id=1127037.1127039","DOI":"10.1016\/j.scico.2005.03.007"},{"key":"369_CR17","doi-asserted-by":"crossref","unstructured":"Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: Proceedings of FM \u201909, pp. 321\u2013337. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-05089-3_21"},{"key":"369_CR18","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Proceedings of CHARME \u201999, pp. 219\u2013234. Springer, London (1999)","DOI":"10.1007\/3-540-48153-2_17"},{"key":"369_CR19","unstructured":"Michael, M.M., Scott, M.L.: Correction of a memory management method for lock-free data structures. No. TR-599. University of Rochester, Computer Science Department (1995)"},{"key":"369_CR20","doi-asserted-by":"crossref","unstructured":"Noll, T., Rieger, S.: Verifying dynamic pointer-manipulating threads. In: Proceedings of the 15th International Symposium on Formal Methods, FM \u201908, pp. 84\u201399. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-68237-0_8"},{"key":"369_CR21","doi-asserted-by":"crossref","unstructured":"O\u2019Leary, J., Talupur, M., Tuttle, M.: Protocol verification using flows: An industrial experience. In: Proeedings of Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 172\u2013179 (2009)","DOI":"10.1109\/FMCAD.2009.5351126"},{"key":"369_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants, TACAS 2001, pp. 82\u201397. Springer, London (2001)","DOI":"10.1007\/3-540-45319-9_7"},{"key":"369_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-counter abstraction. In: Proceedings of the 14th International Conference on Computer Aided Verification, CAV \u201902, pp. 107\u2013122. Springer London (2002)","DOI":"10.1007\/3-540-45657-0_9"},{"key":"369_CR24","volume-title":"Intel Threading Building Blocks","author":"J Reinders","year":"2007","unstructured":"Reinders, J.: Intel Threading Building Blocks, 1st edn. O\u2019Reilly & Associates Inc, Sebastopol (2007)","edition":"1"},{"key":"369_CR25","doi-asserted-by":"crossref","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 \u201999, pp. 105\u2013118. ACM, New York (1999)","DOI":"10.1145\/292540.292552"},{"key":"369_CR26","doi-asserted-by":"crossref","unstructured":"Sethi, D., Talupur, M., Schwartz-Narbonne, D., Malik, S.: Parameterized model checking of fine grained concurrency. In: Proceedings of 19th International SPIN Workshop on Model Checking of Software (2012)","DOI":"10.1007\/978-3-642-31759-0_15"},{"key":"369_CR27","doi-asserted-by":"crossref","unstructured":"Talupur, M., Tuttle, M.: Going with the flow: Parameterized verification using message flows. In: Proceedings of Formal Methods in Computer-Aided Design, FMCAD \u201908, pp. 1\u20138 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"369_CR28","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability, VMCAI \u201909, pp. 335\u2013348. Springer, Berlin (2009)","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"369_CR29","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Proceedings of Computer Aided Verification, pp. 450\u2013464 (2010)","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"369_CR30","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: Proceedings of PPoPP \u201906, pp. 129\u2013136. ACM, New York (2006)","DOI":"10.1145\/1122971.1122992"},{"key":"369_CR31","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: Proceedings of the 16th International SPIN Workshop on Model Checking Software, pp. 261\u2013278. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02652-2_21"},{"key":"369_CR32","doi-asserted-by":"crossref","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 \u201901, pp. 27\u201340. ACM, New York (2001)","DOI":"10.1145\/373243.360206"},{"key":"369_CR33","doi-asserted-by":"crossref","unstructured":"Zhang, S.J.: Scalable automatic linearizability checking. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE \u201911, pp. 1185\u20131187. ACM, New York (2011)","DOI":"10.1145\/1985793.1986037"},{"key":"369_CR34","doi-asserted-by":"crossref","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 \u201910, pp. 43\u201352. IEEE Computer Society, Washington DC (2010)","DOI":"10.1109\/SSIRI.2010.37"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0369-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0369-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0369-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T00:15:55Z","timestamp":1566346555000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0369-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,15]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,8]]}},"alternative-id":["369"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0369-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,15]]}}}