{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:28:08Z","timestamp":1750188488669},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319336923"},{"type":"electronic","value":"9783319336930"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33693-0_13","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T01:35:47Z","timestamp":1464053747000},"page":"193-209","source":"Crossref","is-referenced-by-count":8,"title":["Towards a Thread-Local Proof Technique for Starvation Freedom"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[]},{"given":"Oleg","family":"Travkin","sequence":"additional","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"issue":"3","key":"13_CR1","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3), 507\u2013534 (1995)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR2","volume-title":"Beauty is Our Business - A Birthday Salute to Edsger W. Dijkstra","author":"KR Apt","year":"1990","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.-R.: Proving termination of parallel programs. In: Feijen, W.H.J., van Gasteren, A.J.M., Gries, D., Misra, J. (eds.) Beauty is Our Business - A Birthday Salute to Edsger W. Dijkstra. Springer, New York (1990)"},{"issue":"6","key":"13_CR3","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"13_CR4","unstructured":"Bostr\u00f6m, P., M\u00fcller, P.: Modular verification of finite blocking in non-terminating programs. In: ECOOP, LIPIcs, vol. 37, pp. 639\u2013663 (2015)"},{"key":"13_CR5","unstructured":"de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press, Cambridge (2001)"},{"key":"13_CR6","first-page":"1","volume":"17","author":"G Ernst","year":"2014","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV - overview and VerifyThis competition. Softw. Tools Technol. Transf. 17, 1\u201318 (2014)","journal-title":"Softw. Tools Technol. Transf."},{"issue":"3","key":"13_CR7","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10009-005-0193-x","volume":"8","author":"Y Fang","year":"2006","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with invisible ranking. STTT 8(3), 261\u2013279 (2006)","journal-title":"STTT"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that non-blocking algorithms don\u2019t block. In: POPL, pp. 16\u201328. ACM (2009)","DOI":"10.1145\/1594834.1480886"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/978-3-642-25873-2_22","volume-title":"Principles of Distributed Systems","author":"M Herlihy","year":"2011","unstructured":"Herlihy, M., Shavit, N.: On the nature of progress. In: Fern\u00e0ndez Anta, A., Lipari, G., Roy, M. (eds.) OPODIS 2011. LNCS, vol. 7109, pp. 313\u2013328. Springer, Heidelberg (2011)"},{"key":"13_CR10","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321\u2013332 (1983)"},{"key":"13_CR11","unstructured":"Proofs of starvation freedom in KIV (2015). http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/Starvation-Free.html"},{"issue":"8","key":"13_CR12","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. In: POPL (2016, to appear)","DOI":"10.1145\/2837614.2837635"},{"key":"13_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems - Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, Berlin (1995)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Progress. Published online, Draft (1996)","DOI":"10.1007\/978-1-4612-4222-2"},{"issue":"1","key":"13_CR16","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/103727.103729","volume":"9","author":"JM Mellor-Crummey","year":"1991","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Trans. Comput. Syst. 9(1), 21\u201365 (1991)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"3","key":"13_CR17","doi-asserted-by":"crossref","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. 10(3), 420\u2013455 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR18","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf. 6, 319\u2013340 (1976)","journal-title":"Acta Inf."},{"issue":"3","key":"13_CR19","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-642-28756-5_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Popeea","year":"2012","unstructured":"Popeea, C., Rybalchenko, A.: Compositional termination proofs for multi-threaded programs. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 237\u2013251. Springer, Heidelberg (2012)"},{"key":"13_CR21","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/s10472-013-9389-z","volume":"71","author":"G Schellhorn","year":"2014","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Pf\u00e4hler, J., Reif, W.: RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. (AMAI) 71, 131\u2013174 (2014)","journal-title":"Ann. Math. Artif. Intell. (AMAI)"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/978-3-319-10181-1_22","volume-title":"Integrated Formal Methods","author":"B Tofan","year":"2014","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: A compositional proof method for linearizability applied to a wait-free multiset. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 357\u2013372. Springer, Heidelberg (2014)"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"3\u20134","key":"13_CR24","first-page":"139","volume":"30","author":"LD Zuck","year":"2004","unstructured":"Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. 30(3\u20134), 139\u2013169 (2004)","journal-title":"Comput. Lang. Syst. Struct."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33693-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T14:33:06Z","timestamp":1567953186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33693-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319336923","9783319336930"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33693-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}