{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T06:47:39Z","timestamp":1767768459970,"version":"3.48.0"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032137104","type":"print"},{"value":"9783032137111","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-13711-1_2","type":"book-chapter","created":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T06:41:34Z","timestamp":1767768094000},"page":"23-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Liveness to\u00a0Safety for\u00a0Distributed Systems"],"prefix":"10.1007","author":[{"given":"Lenore D.","family":"Zuck","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Arons, T., Pnueli, A., Zuck, L.D.: Parameterized verification by probabilistic abstraction. In: Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7\u201311, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pp. 87\u2013102. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-031-62362-2_30","DOI":"10.1007\/978-3-031-62362-2_30"},{"issue":"3","key":"2_CR2","doi-asserted-by":"publisher","first-page":"853","DOI":"10.1016\/j.jcss.2011.08.003","volume":"78","author":"I Balaban","year":"2012","unstructured":"Balaban, I., Pnueli, A., Sa\u2019ar, Y., Zuck, L.D.: Verification of multi-linked heaps. J. Comput. Syst. Sci. 78(3), 853\u2013876 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/11787006_45","volume-title":"Automata, Languages and Programming","author":"I Balaban","year":"2006","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Invisible safety of distributed protocols. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 528\u2013539. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11787006_45"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-540-69738-1_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I Balaban","year":"2007","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis of single-parent heaps. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 91\u2013105. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_7"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design - A Foundation. Addison-Wesley (1989)","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-41528-4_15","volume-title":"Computer Aided Verification","author":"J Daniel","year":"2016","unstructured":"Daniel, J., Cimatti, A., Griggio, A., Tonetta, S., Mover, S.: Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 271\u2013291. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_15"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/11888116_26","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"Y Fang","year":"2006","unstructured":"Fang, Y., McMillan, K.L., Pnueli, A., Zuck, L.D.: Liveness by invisible invariants. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 356\u2013371. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11888116_26"},{"issue":"4","key":"2_CR8","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1137\/0215074","volume":"15","author":"M Luby","year":"1986","unstructured":"Luby, M.: A simple parallel algorithm for the maximal independent set problem. SIAM J. Comput. 15(4), 1036\u20131053 (1986)","journal-title":"SIAM J. Comput."},{"key":"2_CR9","unstructured":"Nancy, A.: Lynch. In: Distributed Algorithms. Morgan Kaufmann (1996)"},{"key":"2_CR10","unstructured":"Manna, Z.: Mathematical Theory of Computation. Dover Publications (2003)."},{"issue":"1","key":"2_CR11","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 91\u2013130 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"POPL","key":"2_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158114","volume":"2","author":"O Padon","year":"2018","unstructured":"Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. 2(POPL), 1\u201333 (2018)","journal-title":"Proc. ACM Program. Lang."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Schuppan, V., Biere, A.: Liveness checking as safety checking for infinite state spaces. In: Proceedings of the 7th International Workshop on Verification of Infinite-State Systems, INFINITY 2005, San Francisco, CA, USA, August 27, 2005, volume 149 of Electronic Notes in Theoretical Computer Science, pp. 79\u201396. Elsevier (2005)","DOI":"10.1016\/j.entcs.2005.11.018"},{"issue":"3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Lecture Notes in Computer Science","On the Pursuit of Insight and Elegance"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-13711-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T06:41:35Z","timestamp":1767768095000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-13711-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032137104","9783032137111"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-13711-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"8 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}