{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T21:26:14Z","timestamp":1790889974322,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540373766","type":"print"},{"value":"9783540373773","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817949_7","type":"book-chapter","created":{"date-parts":[[2006,8,2]],"date-time":"2006-08-02T19:59:29Z","timestamp":1154548769000},"page":"95-109","source":"Crossref","is-referenced-by-count":12,"title":["Proving Liveness by Backwards Reachability"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ahmed","family":"Rezine","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mayank","family":"Saksena","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1999","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling Global Conditions in Parameterized System Verification. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 134\u2013145. Springer, Heidelberg (1999)"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Yih-Kuen, T.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation\u00a0160, 109\u2013127 (2000)","journal-title":"Information and Computation"},{"issue":"1","key":"7_CR3","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/B:FORM.0000033962.51898.1a","volume":"25","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design\u00a025(1), 39\u201365 (2004)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"7_CR4","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1006\/inco.1996.0083","volume":"130","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Information and Computation\u00a0130(1), 71\u201390 (1996)","journal-title":"Information and Computation"},{"issue":"2","key":"7_CR5","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation\u00a0127(2), 91\u2013101 (1996)","journal-title":"Information and Computation"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-27813-9_27","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular Model Checking for LTL(MSO). In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 348\u2013360. Springer, Heidelberg (2004)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-28644-8_3","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A Survey of Regular Model Checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 35\u201348. Springer, Heidelberg (2004)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape Analysis by Predicate Abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI 2001, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1996","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 1\u201312. Springer, Heidelberg (1996)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-27813-9_29","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract Regular Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 372\u2013386. Springer, Heidelberg (2004)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11539452_37","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A. Bradley","year":"2005","unstructured":"Bradley, A., Manna, Z., Sipma, H.: Linear ranking with reachability. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination analysis of integer linear loops. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 488\u2013502. Springer, Heidelberg (2005)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-30579-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Bradley","year":"2005","unstructured":"Bradley, A., Manna, Z., Sipma, H.: Termination of Polynomial Programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"7_CR15","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)"},{"issue":"5","key":"7_CR16","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. Software Tools for Technology Transfer\u00a02, 279\u2013287 (1999)","journal-title":"Software Tools for Technology Transfer"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Colon","year":"2001","unstructured":"Colon, M., Sipma, H.: Synthesis of Linear Ranking Functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"M. Colon","year":"2002","unstructured":"Colon, M., Sipma, H.: Practical Methods for Proving Program Termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"key":"7_CR20","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":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-540-24730-2_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Fang","year":"2004","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with Incomprehensible Ranking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 482\u2013496. Springer, Heidelberg (2004)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-24622-0_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Fang","year":"2004","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with Invisible Ranking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 223\u2013238. Springer, Heidelberg (2004)"},{"issue":"5","key":"7_CR24","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"SE-23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Trans. on Software Engineering\u00a0SE-23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. 28th ACM Symp. on Principles of Programming Languages, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"issue":"4","key":"7_CR26","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"4","author":"Z. Manna","year":"1984","unstructured":"Manna, Z., Pnueli, A.: Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming\u00a04(4), 257\u2013289 (1984)","journal-title":"Science of Computer Programming"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Tools and rules for the practicing verifier. In: Rashid, R. (ed.) CMU Computer Science: A 25th Anniversary Commemorative, pp. 125\u2013159. ACM Press and Addison-Wesley (1991)","DOI":"10.21236\/ADA227320"},{"key":"7_CR28","unstructured":"Nilsson, M.: Regular Model Checking. PhD thesis, Uppsala University (2005)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-31980-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2005","unstructured":"Pnueli, A., Podelski, A., Rybalchenko, A.: Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 124\u2013139. Springer, Heidelberg (2005)"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/10722167_26","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2000","unstructured":"Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 328\u2013343. Springer, Heidelberg (2000)"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0,1,infinity)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 107. Springer, Heidelberg (2002)"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proc. LICS 2004 20th IEEE Int. Symp. on Logic in Computer Science, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: Proc. 32th ACM Symp. on Principles of Programming Languages, pp. 132\u2013144 (2005)","DOI":"10.1145\/1040305.1040317"},{"key":"7_CR34","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1109\/JCIT.1990.128275","volume-title":"Proc. Fifth Jerusalem Conference on Information Technology","author":"B.K. Szymanski","year":"1990","unstructured":"Szymanski, B.K.: Mutual exclusion revisited. In: Proc. Fifth Jerusalem Conference on Information Technology, pp. 110\u2013117. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2006 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817949_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:15:53Z","timestamp":1605644153000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817949_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540373766","9783540373773"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/11817949_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}