{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:23:09Z","timestamp":1772835789919,"version":"3.50.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,1,23]],"date-time":"2016-01-23T00:00:00Z","timestamp":1453507200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,3]]},"DOI":"10.1007\/s10817-015-9358-9","type":"journal-article","created":{"date-parts":[[2016,1,23]],"date-time":"2016-01-23T00:23:43Z","timestamp":1453508623000},"page":"309-341","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Mechanizing a Process Algebra for Network Protocols"],"prefix":"10.1007","volume":"56","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0601-4182","authenticated-orcid":false,"given":"Timothy","family":"Bourke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert J.","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","published-online":{"date-parts":[[2016,1,23]]},"reference":[{"key":"9358_CR1","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Parrow, J.: Psi-calculi in Isabelle. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2009). LNCS, vol. 5674, pp. 99\u2013114. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03359-9_9"},{"key":"9358_CR2","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: Principles of Programming Languages (POPL\u201906), pp. 55\u201366. ACM (2006)","DOI":"10.1145\/1111320.1111043"},{"key":"9358_CR3","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Conference on Automated Deduction (CADE-23). LNCS, vol. 6803, pp. 116\u2013130. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"9358_CR4","unstructured":"Bourke, T.: Mechanization of the Algebra for Wireless Networks (AWN). Archive of Formal Proofs (2014). http:\/\/afp.sf.net\/entries\/AWN.shtml"},{"key":"9358_CR5","doi-asserted-by":"crossref","unstructured":"Bourke, T., van Glabbeek, R.J., H\u00f6fner, P.: A mechanized proof of loop freedom of the (untimed) AODV routing protocol. In: Cassez, F., Raskin, J.F. (eds.) Automated Technology for Verification and Analysis (ATVA\u201914). LNCS, vol. 8837, pp. 47\u201363. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-11936-6_5"},{"key":"9358_CR6","doi-asserted-by":"crossref","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.) Interactive Theorem Proving (ITP\u201914). LNCS, vol. 8558, pp. 144\u2013159. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-08970-6_10"},{"key":"9358_CR7","unstructured":"Bourke, T., H\u00f6fner, P.: Loop Freedom of the (Untimed) Aodv Routing Protocol. Archive of Formal Proofs (2014). http:\/\/afp.sf.net\/entries\/AODV.shtml"},{"key":"9358_CR8","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, Boston (1988)"},{"key":"9358_CR9","doi-asserted-by":"crossref","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the TLA+ proof system. In: Giesl, J., H\u00e4hnle, R. (eds.) International Joint Conference on Automated Reasoning (IJCAR\u201910). LNCS, vol. 6173, pp. 142\u2013148. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14203-1_12"},{"key":"9358_CR10","doi-asserted-by":"crossref","unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) European Symposium on Programming (ESOP \u201912). LNCS, vol. 7211, pp. 295\u2013315. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28869-2_15"},{"key":"9358_CR11","unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical Report 5513, NICTA (2013). http:\/\/arxiv.org\/abs\/1312.7645"},{"key":"9358_CR12","doi-asserted-by":"crossref","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.) Verified Software: Theories, Tools, and Experiments (VSTTE\u201912) LNCS, vol. 7152, pp. 243\u2013260. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-27705-4_20"},{"key":"9358_CR13","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"R.W. Floyd","year":"1967","unstructured":"Floyd R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19\u201332 (1967)","journal-title":"Proc. Symp. Appl. Math."},{"key":"9358_CR14","first-page":"109","volume":"82","author":"W. Fokkink","year":"2004","unstructured":"Fokkink W., Groote J.F., Reniers M.: Process algebra needs proof methodology. EATCS Bull. 82, 109\u2013125 (2004)","journal-title":"EATCS Bull."},{"key":"9358_CR15","doi-asserted-by":"crossref","unstructured":"Ghassemi, F., Fokkink, W., Movaghar, A.: Restricted broadcast process theory. In: Cerone, A., Gruner, S. (eds.) Software Engineering and Formal Methods (SEFM \u201908), pp. 345\u2013354. IEEE Computer Society (2008)","DOI":"10.1109\/SEFM.2008.25"},{"key":"9358_CR16","doi-asserted-by":"crossref","unstructured":"Godskesen, J.C.: A calculus for mobile ad hoc networks. In: Murphy, A.L., Vitek, J. (eds.) Coordination Models and Languages (COORDINATION \u201907) LNCS, vol. 4467, pp. 132\u2013150. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-72794-1_8"},{"issue":"3","key":"9358_CR17","doi-asserted-by":"crossref","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. Innov. Syst. Softw. Eng. 6(3), 181\u2013193 (2010)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"9358_CR18","doi-asserted-by":"crossref","unstructured":"Heyd, B., Cr\u00e9gut, P.: A modular coding of UNITY in COQ. In: Goos, G., Hartmanis, J., Leeuwen, J., Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 1996) LNCS, vol. 1125, pp. 251\u2013266. Springer, Berlin (1996)","DOI":"10.1007\/BFb0105409"},{"key":"9358_CR19","doi-asserted-by":"crossref","unstructured":"Hirschkoff, D.: A full formalisation of \u03c0-calculus theory in the calculus of constructions. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007). LNCS, vol. 4732, pp. 153\u2013169. Springer, Berlin (2007)","DOI":"10.1007\/BFb0028392"},{"key":"9358_CR20","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales: A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 1999). LNCS, vol. 1690, pp. 149\u2013165. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48256-3_11"},{"key":"9358_CR21","volume-title":"Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers","author":"L. Lamport","year":"2002","unstructured":"Lamport L.: Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers. Addison Wesley, Boston (2002)"},{"key":"9358_CR22","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Q. 2(3), 219\u2013246 (1989). http:\/\/theory.lcs.mit.edu\/tds\/papers\/Lynch\/CWI89.html"},{"key":"9358_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna Z., Pnueli A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin (1995)"},{"issue":"2","key":"9358_CR24","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/j.ic.2007.11.010","volume":"207","author":"M. Merro","year":"2009","unstructured":"Merro M.: An observational theory for mobile ad hoc networks (full version). Inf. Comput. 207(2), 194\u2013208 (2009)","journal-title":"Inf. Comput."},{"key":"9358_CR25","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1016\/j.entcs.2006.04.017","volume":"158","author":"N. Mezzetti","year":"2006","unstructured":"Mezzetti N., Sangiorgi D.: Towards a calculus for wireless systems. Electron. Notes Theor. Comput. Sci. (ENTCS) 158, 331\u2013353 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci. (ENTCS)"},{"key":"9358_CR26","doi-asserted-by":"crossref","unstructured":"Milner, R.: Operational and algebraic semantics of concurrent processes. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, chap. 19, pp. 1201\u20131242. Elsevier Science Publishers B.V. (North-Holland) (1990). Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems. LNCS 92, Springer, 1980","DOI":"10.1016\/B978-0-444-88074-1.50024-X"},{"key":"9358_CR27","unstructured":"M\u00fcller, O.: A Verification Environment for I\/O Automata Based on Formalized Meta-theory. Ph.D. Thesis, TU M\u00fcnchen (1998)"},{"key":"9358_CR28","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/j.tcs.2006.08.036","volume":"367","author":"S. Nanz","year":"2006","unstructured":"Nanz S., Hankin C.: A framework for security analysis of mobile wireless networks. Theor. Comput. Sci. 367, 203\u2013227 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"9358_CR29","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"1\u20132","key":"9358_CR30","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. Comput. Secur. 6(1\u20132), 85\u2013128 (1998)","journal-title":"J. Comput. Secur."},{"key":"9358_CR31","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)","DOI":"10.17487\/rfc3561"},{"key":"9358_CR32","doi-asserted-by":"crossref","unstructured":"Plotkin, G.: A structural approach to operational semantics. J. Log. Algebr. Program. 60\u201361, 17\u2013139 (2004). Originally appeared in 1981","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"9358_CR33","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 54. CUP (2001)"},{"key":"9358_CR34","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1016\/j.scico.2009.07.008","volume":"75","author":"A. Singh","year":"2010","unstructured":"Singh A., Ramakrishnan C.R., Smolka S.A.: A process calculus for mobile ad hoc networks. Sci. Comput. Program. 75, 440\u2013469 (2010)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"9358_CR35","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"key":"9358_CR36","doi-asserted-by":"crossref","unstructured":"Tej, H., Wolff, B.: A corrected failure divergence model for CSP in Isabelle\/HOL. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) Industrial Applications and Strengthened Foundations of Formal Methods (FME\u201997). LNCS, vol. 1313, pp. 318\u2013337. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63533-5_17"},{"key":"9358_CR37","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isabelle\/jEdit\u2014a prover IDE within the PIDE framework. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) Intelligent Computer Mathematics. LNCS, vol. 7362, pp. 468\u2013471. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31374-5_38"},{"key":"9358_CR38","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Shared-memory multiprocessing for interactive theorem proving. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving (ITP\u201913). LNCS, vol. 7998, pp. 418\u2013434. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39634-2_30"},{"key":"9358_CR39","doi-asserted-by":"crossref","unstructured":"Zhou, M., Yang, H., Zhang, X., Wang, J.: The proof of AODV loop freedom. In: International Conference on Wireless Communications and Signal Processing (WCSP\u201909). IEEE (2009)","DOI":"10.1109\/WCSP.2009.5371479"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9358-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9358-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9358-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,3]],"date-time":"2019-09-03T19:27:45Z","timestamp":1567538865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9358-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,23]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["9358"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9358-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1,23]]}}}