{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:27:52Z","timestamp":1772836072735,"version":"3.50.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319119359","type":"print"},{"value":"9783319119366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_5","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T15:11:50Z","timestamp":1414163510000},"page":"47-63","source":"Crossref","is-referenced-by-count":11,"title":["A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol"],"prefix":"10.1007","author":[{"given":"Timothy","family":"Bourke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rob","family":"van Glabbeek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-03359-9_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Bengtson","year":"2009","unstructured":"Bengtson, J., Parrow, J.: Psi-calculi in Isabelle. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 99\u2013114. Springer, Heidelberg (2009)"},{"issue":"4","key":"5_CR2","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":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. In: POPL 2006, pp. 55\u201366. ACM (2006)","DOI":"10.1145\/1111320.1111043"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-08970-6_10","volume-title":"Interactive Theorem Proving","author":"T. Bourke","year":"2014","unstructured":"Bourke, T., van Glabbeek, R.J., H\u00f6fner, P.: Showing invariance compositionally for a process algebra for network protocols. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol.\u00a08558, pp. 144\u2013159. Springer, Heidelberg (2014)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bourke, T., H\u00f6fner, P.: Loop freedom of the (untimed) AODV routing protocol. Archive of Formal Proofs (2014), \n                  \n                    http:\/\/afp.sf.net\/entries\/AODV.shtml","DOI":"10.1007\/978-3-319-11936-6_5"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-14203-1_12","volume-title":"Automated Reasoning","author":"K. Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the TLA\u2009+\u2009 proof system. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 142\u2013148. Springer, Heidelberg (2010)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0028390","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Dutertre","year":"1997","unstructured":"Dutertre, B., Schneider, S.: Using a PVS embedding of CSP to verify authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 121\u2013136. Springer, Heidelberg (1997)"},{"key":"5_CR8","unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical Report 5513, NICTA (2013), \n                  \n                    http:\/\/arxiv.org\/abs\/1312.7645"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-27705-4_20","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A. Feliachi","year":"2012","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle\/Circus: A process specification and verification environment. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 243\u2013260. Springer, Heidelberg (2012)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J., H\u00f6fner, P., Tan, W.L., Portmann, M.: Sequence numbers do not guarantee loop freedom \u2014AODV can yield routing loops\u2014. In: MSWiM 2013, pp. 91\u2013100. ACM (2013)","DOI":"10.1145\/2507924.2507943"},{"issue":"3","key":"5_CR11","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s11334-010-0126-z","volume":"6","author":"T. G\u00f6thel","year":"2010","unstructured":"G\u00f6thel, T., Glesner, S.: An approach for machine-assisted verification of Timed CSP specifications. Innovations in Systems and Software Engineering\u00a06(3), 181\u2013193 (2010)","journal-title":"Innovations in Systems and Software Engineering"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BFb0105409","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Heyd","year":"1996","unstructured":"Heyd, B., Cr\u00e9gut, P.: A modular coding of UNITY in COQ. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 251\u2013266. Springer, Heidelberg (1996)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0028392","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Hirschkoff","year":"1997","unstructured":"Hirschkoff, D.: A full formalisation of \u03c0-calculus theory in the Calculus of Constructions. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 153\u2013169. Springer, Heidelberg (1997)"},{"key":"5_CR14","unstructured":"IEEE: IEEE standard for information technology\u2014telecommunications and information exchange between systems\u2014local and metropolitan area networks\u2014specific requirements part 11: Wireless LAN medium access control (MAC) and physical layer (PHY) specifications amendment 10: Mesh networking (2011)"},{"key":"5_CR15","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Miskovic, S., Knightly, E.W.: Routing primitives for wireless mesh networks: Design, analysis and experiments. In: INFOCOM 2010, pp. 2793\u20132801. IEEE (2010)","DOI":"10.1109\/INFCOM.2010.5462111"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BFb0055145","volume-title":"Theorem Proving in Higher Order Logics","author":"O. M\u00fcller","year":"1998","unstructured":"M\u00fcller, O.: I\/O automata and beyond: Temporal logic and abstraction in Isabelle. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 331\u2013348. Springer, Heidelberg (1998)"},{"key":"5_CR19","unstructured":"M\u00fcller, O.: A Verification Environment for I\/O Automata Based on Formalized Meta-Theory. Ph.D. thesis, TU M\u00fcnchen (1998)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"1-2","key":"5_CR21","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Computer Security\u00a06(1-2), 85\u2013128 (1998)","journal-title":"J. Computer Security"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Perkins, C.E., Royer, E.M.: Ad-hoc On-Demand Distance Vector Routing. In: Mobile Computing Systems and Applications (WMCSA 1999), pp. 90\u2013100. IEEE (1999)","DOI":"10.1109\/MCSA.1999.749281"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Perkins, C.E., Belding-Royer, E.M., Das, S.R.: Ad hoc on-demand distance vector (AODV) routing. RFC 3561 (Experimental), Network Working Group (2003), \n                  \n                    http:\/\/www.ietf.org\/rfc\/rfc3561.txt","DOI":"10.17487\/rfc3561"},{"key":"5_CR24","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.\u00a054. Cambridge University Press (2001)"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Schirmer, N., Wenzel, M.: State spaces\u2014the locale way. In: Huuck, R., Klein, G., Schlich, B. (eds.) SSV 2009. ENTCS, vol.\u00a0254, pp. 161\u2013179. Elsevier (2009)","DOI":"10.1016\/j.entcs.2009.09.065"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Zhou, M., Yang, H., Zhang, X., Wang, J.: The proof of AODV loop freedom. In: WCSP 2009. IEEE (2009)","DOI":"10.1109\/WCSP.2009.5371479"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T03:05:13Z","timestamp":1559012713000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}