@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,
}
