{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:22:03Z","timestamp":1757312523238},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642287558"},{"type":"electronic","value":"9783642287565"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_17","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:57:15Z","timestamp":1332449835000},"page":"237-251","source":"Crossref","is-referenced-by-count":26,"title":["Compositional Termination Proofs for Multi-threaded Programs"],"prefix":"10.1007","author":[{"given":"Corneliu","family":"Popeea","sequence":"first","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-540-73368-3_9","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2007","unstructured":"Cohen, A., Namjoshi, K.S.: Local Proofs for Global Safety Properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 55\u201367. Springer, Heidelberg (2007)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-70545-1_15","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2008","unstructured":"Cohen, A., Namjoshi, K.S.: Local Proofs for Linear-Time Properties of Concurrent Programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 149\u2013161. Springer, Heidelberg (2008)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-642-14295-6_46","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2010","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y.: A Dash of Fairness for Compositional Reasoning. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 543\u2013557. Springer, Heidelberg (2010)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction Refinement for Termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving thread termination. In: PLDI (2007)","DOI":"10.1145\/1250734.1250771"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-45927-8_19","volume-title":"Programming Languages and Systems","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-Modular Verification for Shared-Memory Programs. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 262\u2013277. Springer, Heidelberg (2002)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI (2007)","DOI":"10.1145\/1250734.1250765"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that non-blocking algorithms don\u2019t block. In: POPL (2009)","DOI":"10.1145\/1594834.1480886"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL (2011)","DOI":"10.1145\/1926385.1926424"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI (2004)","DOI":"10.1145\/996841.996844"},{"issue":"4","key":"17_CR13","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst.\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-14295-6_9","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2010","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination Analysis with Compositional Transition Invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 89\u2013103. Springer, Heidelberg (2010)"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: ASPLOS (2008)","DOI":"10.1145\/1346281.1346323"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"issue":"3","key":"17_CR17","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1145\/44501.44504","volume":"10","author":"E.-R. Olderog","year":"1988","unstructured":"Olderog, E.-R., Apt, K.R.: Fairness in parallel programs: The transformational approach. ACM Trans. Program. Lang. Syst.\u00a010(3), 420\u2013455 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyzer for Java bytecode based on path-length. ACM Trans. Program. Lang. Syst. (2010)","DOI":"10.1145\/1709093.1709095"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:08:48Z","timestamp":1620126528000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}