{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:23:06Z","timestamp":1772835786974,"version":"3.50.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319191942","type":"print"},{"value":"9783319191959","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19195-9_7","type":"book-chapter","created":{"date-parts":[[2015,5,5]],"date-time":"2015-05-05T06:28:41Z","timestamp":1430807321000},"page":"98-112","source":"Crossref","is-referenced-by-count":9,"title":["Loop Freedom in AODVv2"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard J.","family":"Trefler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"7_CR1","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1145\/581771.581775","volume":"49","author":"K. Bhargavan","year":"2002","unstructured":"Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM\u00a049(4), 538\u2013576 (2002)","journal-title":"J. ACM"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1007\/978-3-540-71209-1_54","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2007","unstructured":"Bouajjani, A., Jurski, Y., Sighireanu, M.: A generic framework for reasoning about dynamic networks of infinite-state processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 690\u2013705. Springer, Heidelberg (2007)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Chandy, K., Misra, J.: Proofs of networks of processes. IEEE Transactions on Software Engineering\u00a07(4) (1981)","DOI":"10.1109\/TSE.1981.230844"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988)","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-36126-X_2","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Das","year":"2002","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 19\u201332. Springer, Heidelberg (2002)"},{"key":"7_CR6","unstructured":"Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS. LIPIcs, vol.\u00a018, pp. 289\u2013300. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of safety properties in ad hoc network protocols. In: PACO. EPTCS, vol.\u00a060, pp. 56\u201365 (2011)","DOI":"10.4204\/EPTCS.60.4"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-30793-5_15","volume-title":"Formal Techniques for Distributed Systems","author":"G. Delzanno","year":"2012","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of ad hoc networks with node and communication failures. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE 2012. LNCS, vol.\u00a07273, pp. 235\u2013250. Springer, Heidelberg (2012)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Edenhofer, S., H\u00f6fner, P.: Towards a rigorous analysis of AODVv2 (DYMO). In: 20th IEEE International Conference on Network Protocols, ICNP 2012, Austin, TX, USA, October 30-November 2, pp. 1\u20136. IEEE (2012)","DOI":"10.1109\/ICNP.2012.6459942"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-28756-5_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Fehnker","year":"2012","unstructured":"Fehnker, A., van Glabbeek, R., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 173\u2013187. Springer, Heidelberg (2012)"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"H\u00f6fner, P., van Glabbeek, R.J., Tan, W.L., Portmann, M., McIver, A., Fehnker, A.: A rigorous analysis of AODV and its variants. In: MSWiM, pp. 203\u2013212. ACM (2012)","DOI":"10.1145\/2387238.2387274"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-662-46681-0_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.S. Namjoshi","year":"2015","unstructured":"Namjoshi, K.S., Trefler, R.J.: Analysis of dynamic process networks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol.\u00a09035, pp. 164\u2013178. Springer, Heidelberg (2015)"},{"issue":"5","key":"7_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Commun. ACM\u00a019(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"key":"7_CR14","unstructured":"Perkins, C., Ratliff, S., Dowdell, J.: IETF MANET WG Internet Draft (December 2014), \n                      \n                        http:\/\/datatracker.ietf.org\/doc\/draft-ietf-manet-aodvv2\n                      \n                      \n                    , current revision 06"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular reasoning about programs. In: Logics and Models of Concurrent Systems. NATO ASI Series (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-78800-3_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Saksena","year":"2008","unstructured":"Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 18\u201332. Springer, Heidelberg (2008)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J., H\u00f6fner, P., Tan, W.L., Portmann, M.: Sequence numbers do not guarantee loop freedom \u2013 AODV can yield routing loops \u2013. In: MSWiM, 10 pages. ACM (2013)","DOI":"10.1145\/2507924.2507943"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19195-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T19:48:56Z","timestamp":1559159336000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-19195-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319191942","9783319191959"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19195-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}