{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:07:01Z","timestamp":1748750821474,"version":"3.41.0"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319262864"},{"type":"electronic","value":"9783319262871"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-26287-1_9","type":"book-chapter","created":{"date-parts":[[2015,10,26]],"date-time":"2015-10-26T05:44:58Z","timestamp":1445838298000},"page":"139-154","source":"Crossref","is-referenced-by-count":0,"title":["Limited Mobility, Eventual Stability"],"prefix":"10.1007","author":[{"given":"Lenore D.","family":"Zuck","sequence":"first","affiliation":[]},{"given":"Sanjiva","family":"Prasad","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,28]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1023\/A:1008734618526","volume":"17","author":"RM Amadio","year":"2000","unstructured":"Amadio, R.M., Prasad, S.: Modelling IP mobility. Formal Methods Syst. Design 17(1), 61\u201399 (2000)","journal-title":"Formal Methods Syst. Design"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 221. Springer, Heidelberg (2001)"},{"issue":"3","key":"9_CR3","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":"9_CR4","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)"},{"key":"9_CR5","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)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Dang, Z., Kemmerer, R.A.: Using the ASTRAL model checker to analyze mobile IP. In: Proceedings of the 1999 International Conference on Software Engineering, ICSE 1999, Los Angeles, 16\u201322 May 1999, pp. 132\u2013142 (1999)","DOI":"10.1145\/302405.302459"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Proceedings Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, 17\u201320 June 2000, pp. 236\u2013254 (2000)","DOI":"10.1007\/10721959_19"},{"key":"9_CR8","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)"},{"issue":"3","key":"9_CR9","doi-asserted-by":"publisher","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"},{"issue":"1","key":"9_CR10","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1006\/inco.2001.3085","volume":"173","author":"TA Henzinger","year":"2002","unstructured":"Henzinger, T.A., Kupferman, O., Rajamani, S.K.: Fair simulation. Inf. Comput. 173(1), 64\u201381 (2002)","journal-title":"Inf. Comput."},{"issue":"6","key":"9_CR11","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/s001659970001","volume":"11","author":"D Jackson","year":"1999","unstructured":"Jackson, D., Ng, Y.-C., Wing, J.M.: A nitpick analysis of mobile IPv6. Formal Aspects Comput. 11(6), 591\u2013615 (1999)","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"9_CR12","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Inf. Comput. 163(1), 203\u2013243 (2000)","journal-title":"Inf. Comput."},{"issue":"2","key":"9_CR13","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1145\/304399.304400","volume":"8","author":"PJ McCann","year":"1999","unstructured":"McCann, P.J., Roman, G.-C.: Modeling mobile IP in mobile unity. ACM Trans. Softw. Eng. Methodol. 8(2), 115\u2013146 (1999)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Perkins, C., Johnson, D., Arkko, J.: Mobility Support in IPv6. RFC 6275 (Proposed Standard), July 2011","DOI":"10.17487\/rfc6275"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 82. Springer, Heidelberg (2001)"},{"key":"9_CR16","unstructured":"Rodrigues, C.L., Guerra, F.V., de Figueiredo, J.C.A., Guerrero, D.D.S., Morais, T.S.: Modeling and verification of mobility issues using object-oriented petri nets. In: Proceedings of 3rd International Information and Telecommunication Technologies Symposium (I2TS2004) (2004)"},{"issue":"3\u20134","key":"9_CR17","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","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-26287-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:12:49Z","timestamp":1748664769000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-26287-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319262864","9783319262871"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-26287-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}