{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:46:40Z","timestamp":1777348000647,"version":"3.51.4"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319667058","type":"print"},{"value":"9783319667065","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-66706-5_9","type":"book-chapter","created":{"date-parts":[[2017,8,18]],"date-time":"2017-08-18T04:13:26Z","timestamp":1503029606000},"page":"169-191","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Effect Summaries for Thread-Modular Analysis"],"prefix":"10.1007","author":[{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Wolff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,19]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: LICS. pp. 165\u2013175. IEEE, Las Vegas (1988)","DOI":"10.1109\/LICS.1988.5115"},{"key":"9_CR2","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. LNCS, vol. 7795, pp. 324\u2013338. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_23"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-662-53413-7_4","volume-title":"Static Analysis","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Jonsson, B., Trinh, C.Q.: Automated verification of linearization policies. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 61\u201383. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-53413-7_4"},{"key":"9_CR4","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. 5123, pp. 399\u2013413. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-70545-1_37"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: a technique to pass information between verifiers. In: SIGSOFT FSE. p. 57. ACM, New York (2012)","DOI":"10.1145\/2393596.2393664"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-662-53413-7_6","volume-title":"Static Analysis","author":"M Christakis","year":"2016","unstructured":"Christakis, M., W\u00fcstholz, V.: Bounded abstract interpretation. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 105\u2013125. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-53413-7_6"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 235\u2013249. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23217-6_16"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: FORTE. LNCS, vol. 3235, pp. 97\u2013114. Springer, New York (2004)","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-642-12002-2_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Elmas","year":"2010","unstructured":"Elmas, T., Qadeer, S., Sezgin, A., Subasi, O., Tasiran, S.: Simplifying linearizability proofs with reduction and abstraction. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 296\u2013311. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-12002-2_25"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL. pp. 2\u201315. ACM, New York (2009)","DOI":"10.1145\/1594834.1480885"},{"key":"9_CR11","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. 2648, pp. 213\u2013224. Springer, Heidelberg (2003). doi: 10.1007\/3-540-44829-2_14"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI. pp. 266\u2013277. ACM, New York (2007)","DOI":"10.1145\/1273442.1250765"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-37036-6_15","volume-title":"Programming Languages and Systems","author":"A Gotsman","year":"2013","unstructured":"Gotsman, A., Rinetzky, N., Yang, H.: Verifying concurrent memory reclamation algorithms with grace. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 249\u2013269. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-37036-6_15"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-662-49122-5_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Haziza","year":"2016","unstructured":"Haziza, F., Hol\u00edk, L., Meyer, R., Wolff, S.: Pointer race freedom. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 393\u2013412. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49122-5_19"},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM TOPLAS 12(3), 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"key":"9_CR16","unstructured":"Hol\u00edk, L., Meyer, R., Vojnar, T., Wolff, S.: Effect summaries for thread-modular analysis. CoRR abs\/1705.03701 (2017). http:\/\/arxiv.org\/abs\/1705.03701"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Jagannathan, S., Petri, G., Vitek, J., Pichardie, D., Laporte, V.: Atomicity refinement for verified compilation. In: PLDI, p. 27. ACM, New York (2014)","DOI":"10.1145\/2666356.2594346"},{"key":"9_CR18","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP, pp. 321\u2013332 (1983)"},{"issue":"4","key":"9_CR19","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5(4), 596\u2013619 (1983)","journal-title":"ACM TOPLAS"},{"issue":"4\u20136","key":"9_CR20","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/s00165-012-0250-7","volume":"24","author":"B Jonsson","year":"2012","unstructured":"Jonsson, B.: Using refinement calculus techniques to prove linearizability. Formal Asp. Comput. 24(4\u20136), 537\u2013554 (2012)","journal-title":"Formal Asp. Comput."},{"issue":"4","key":"9_CR21","first-page":"363","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. JAR 43(4), 363\u2013446 (2009)","journal-title":"A formally verified compiler back-end. JAR"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/11921240_13","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"A Malkis","year":"2006","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular verification is cartesian abstract interpretation. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 183\u2013197. Springer, Heidelberg (2006). doi: 10.1007\/11921240_13"},{"issue":"1","key":"9_CR23","first-page":"1","volume":"51","author":"MM Michael","year":"1998","unstructured":"Michael, M.M., Scott, M.L.: Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors. JPDC 51(1), 1\u201326 (1998)","journal-title":"JPDC"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-19718-5_21","volume-title":"Programming Languages and Systems","author":"A Min\u00e9","year":"2011","unstructured":"Min\u00e9, A.: Static analysis of run-time errors in embedded critical parallel C programs. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 398\u2013418. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19718-5_21"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-54013-4_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Min\u00e9","year":"2014","unstructured":"Min\u00e9, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 39\u201358. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54013-4_3"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-52234-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Monat","year":"2017","unstructured":"Monat, R., Min\u00e9, A.: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 386\u2013404. Springer, Cham (2017). doi: 10.1007\/978-3-319-52234-0_21"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Popeea, C., Rybalchenko, A., Wilhelm, A.: Reduction for compositional verification of multi-threaded programs. In: FMCAD, pp. 187\u2013194. IEEE, New York (2014)","DOI":"10.1109\/FMCAD.2014.6987612"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P Rocha Pinto","year":"2014","unstructured":"Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-44202-9_9"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for linearizability of concurrent data structures. ACM TOCL 15(4), 31:1\u201331:37 (2014)","DOI":"10.1145\/2629496"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-10672-9_5","volume-title":"Programming Languages and Systems","author":"M Segalov","year":"2009","unstructured":"Segalov, M., Lev-Ami, T., Manevich, R., Ganesan, R., Sagiv, M.: Abstract transformers for thread correlation analysis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 30\u201346. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-10672-9_5"},{"key":"9_CR31","unstructured":"Treiber, R.: Systems programming: coping with parallelism. Technical report RJ 5118, IBM (1986)"},{"key":"9_CR32","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":"2008","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 335\u2013348. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-93900-9_27"},{"key":"9_CR33","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). doi: 10.1007\/978-3-642-14295-6_40"},{"key":"9_CR34","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). doi: 10.1007\/978-3-642-11319-2_25"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74407-8_18"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Zhang, S.J., Liu, Y.: Model checking a lazy concurrent list-based set algorithm. In: SSIRI, pp. 43\u201352. IEEE, New York (2010)","DOI":"10.1109\/SSIRI.2010.37"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66706-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T23:21:05Z","timestamp":1750807265000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66706-5_9"}},"subtitle":["Sound Analysis Despite an Unsound Heuristic"],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319667058","9783319667065"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66706-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 August 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 September 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/staticanalysis.org\/sas2017\/sas2017.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}