{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:20Z","timestamp":1776305060509,"version":"3.50.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216676","type":"print"},{"value":"9783319216683","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_1","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T11:08:53Z","timestamp":1436785733000},"page":"3-19","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Poling: SMT Aided Linearizability Proofs"],"prefix":"10.1007","author":[{"given":"He","family":"Zhu","sequence":"first","affiliation":[]},{"given":"Gustavo","family":"Petri","sequence":"additional","affiliation":[]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-36742-7_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 324\u2013338. Springer, Heidelberg (2013)"},{"key":"1_CR2","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., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 477\u2013490. Springer, Heidelberg (2007)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-642-21437-0_25","volume-title":"FM 2011: Formal Methods","author":"J Derrick","year":"2011","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Verifying linearisability with potential linearisation points. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 323\u2013337. Springer, Heidelberg (2011)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"1_CR5","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. 3235, pp. 97\u2013114. Springer, Heidelberg (2004)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-39799-8_11","volume-title":"Computer Aided Verification","author":"C Dr\u0103goi","year":"2013","unstructured":"Dr\u0103goi, C., Gupta, A., Henzinger, T.A.: Automatic linearizability proofs of concurrent objects with cooperating updates. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 174\u2013190. Springer, Heidelberg (2013)"},{"key":"1_CR7","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"I Filipovic","year":"2010","unstructured":"Filipovic, I., O\u2019Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411, 252\u2013266 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-36108-1_18","volume-title":"DISC 2002","author":"TL Harris","year":"2002","unstructured":"Harris, T.L., Fraser, K., Pratt, I.A.: A practical multi-word compare-and-swap operation. In: Malkhi, D. (ed.) DISC 2002. LNCS, vol. 2508, pp. 265\u2013279. Springer, Heidelberg (2002)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/11795490_3","volume-title":"Principles of Distributed Systems","author":"S Heller","year":"2006","unstructured":"Heller, S., Herlihy, M.P., Luchangco, V., Moir, M., Scherer III, W.N., Shavit, N.N.: A lazy concurrent list-based set algorithm. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol. 3974, pp. 3\u201316. Springer, Heidelberg (2006)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. In: SPAA (2004)","DOI":"10.1145\/1007912.1007944"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-40184-8_18","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"TA Henzinger","year":"2013","unstructured":"Henzinger, T.A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. LNCS, vol. 8052, pp. 242\u2013256. Springer, Heidelberg (2013)"},{"key":"1_CR12","volume-title":"The Art of Multiporcessor Programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiporcessor Programming. MorganKaufmann, San Francisco (2008)"},{"issue":"3","key":"1_CR13","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.: Linearizability: a correctness condition for concurrent objects. ACM TOPLAS 12(3), 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: PLDI (2013)","DOI":"10.1145\/2491956.2462189"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC (1996)","DOI":"10.21236\/ADA309412"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Rinetzky, N., Vechev, M., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: PODC (2010)","DOI":"10.1145\/1835698.1835722"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI (2013)","DOI":"10.1145\/2491956.2462169"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-31424-7_21","volume-title":"Computer Aided Verification","author":"G Schellhorn","year":"2012","unstructured":"Schellhorn, G., Wehrheim, H., Derrick, J.: How to prove algorithms linearisable. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 243\u2013259. Springer, Heidelberg (2012)"},{"key":"1_CR19","unstructured":"Treiber, P.: System programming: coping with parallelism. In: Technique report RJ 5118, IBM Almaden Research Center (1986)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Turon, A., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: POPL (2013)","DOI":"10.1145\/2429069.2429111"},{"key":"1_CR21","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge (2008)"},{"key":"1_CR22","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. 6174, pp. 450\u2013464. Springer, Heidelberg (2010)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-11319-2_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: RGSep action inference. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 345\u2013361. Springer, Heidelberg (2010)"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E.: Deriving linerizable fine-grained concurrent objects. In: PLDI (2008)","DOI":"10.1145\/1375581.1375598"},{"key":"1_CR25","unstructured":"Zhu, H., Petri, G., Jagannathan, S.: Poling: Smt aided linearizability proofs. Technical report, Purdue Univsersity (2015). \n                      https:\/\/www.cs.purdue.edu\/homes\/zhu103\/poling\/tech.pdf"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:12:20Z","timestamp":1563826340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}