
@inproceedings{BourkeEtAl:MechAWN:2014,
  author      = {Bourke, T. and van Glabbeek, R. J. and H{\"o}fner, P.},
  title	      = {Showing invariance compositionally for a process algebra for network protocols},
  url	      = {https://doi.org/10.1007/978-3-319-08970-6_10},
  pages =	{144--159},
  booktitle =	{Proceedings of the 5th International Conference on
		 Interactive Theorem Proving (ITP 2014)},
  year =	2014,
  editor =	{Klein, Gerwin and Gamboa, Ruben},
  series =	{Lecture Notes in Computer Science},
  volume =	8558,
  address =	{Vienna, Austria},
  month =	jul,
  publisher =	{Springer},
}

@article{Bourke14,
  author      = {Bourke, T.},
  journal     = {Archive of Formal Proofs},
  note        = {\url{http://isa-afp.org/entries/AWN.shtml}},
  title       = {Mechanization of the {Algebra for Wireless Networks} {(AWN)}},
  year        = 2014
}

@techreport{FehnkerEtAl:AWN:2013,
  author      = {Ansgar Fehnker
	         and van Glabbeek, Robert J.
	         and Peter H{\"{o}}fner
	         and Annabelle McIver
	         and Marius Portmann
	         and Tan, Wee Lum},
  institution = {NICTA},
  number      = 5513,
  title       = {A Process Algebra for Wireless Mesh Networks used for
		 Modelling, Verifying and Analysing {AODV}},
  type        = {Technical Report},
  url         = {http://www.nicta.com.au/pub?doc=5513},
  Year        = 2013,
}

@inproceedings{BourkevGlHof:ATVA:2014,
  author =	{Bourke, Timothy and van Glabbeek, Robert J.
		 and H{\"o}fner, Peter},
  title =	{A mechanized proof of loop freedom of the (untimed) {AODV}
		 routing protocol},
  crossref =    {ATVA2014},
  pages =	{47--63},
  year =	2014,
}

@proceedings{ATVA2014,
  title =	"Proceedings of the 12th International Conference on
		 Automated Technology for Verification and Analysis
		 (ATVA 2014)",
  booktitle =	"Proceedings of the 12th International Conference on
		 Automated Technology for Verification and Analysis
		 (ATVA 2014)",
  year =	2014,
  editor =	{Cassez, Franck and Raskin, Jean-François},
  volume =	8837,
  series =	{Lecture Notes in Computer Science},
  address =	{Sydney, Australia},
  month =	nov,
  publisher =	{Springer},
}

@misc{RFC3561,
  author =	{Charles E. Perkins and Elizabeth M. Belding-Royer and Samir R. Das},
  howpublished = {RFC 3561 (Experimental), Network Working Group},
  number =	3561,
  title =	{Ad hoc On-Demand Distance Vector {(AODV)} Routing},
  type =	{Request for Comments},
  url =		{http://www.ietf.org/rfc/rfc3561.txt},
  year =	2003,
}

@inproceedings{MK10,
  author =	{Miskovic, S. and Knightly, E. W.},
  booktitle =	{Conference on Information Communications {(INFOCOM '10)}},
  pages =	{2793--2801},
  publisher =	{{IEEE}},
  title =	{Routing Primitives for Wireless Mesh Networks: Design,
		 Analysis and Experiments},
  year =	2010,
}

