@inproceedings(Ahrenholz08,
 author       = {J. Ahrenholz and C. Danilov and T. Henderson and J. Kim},
 year         = {2008},
 title        = {{CORE:} A Real-Time Network Emulator},
 booktitle    = {IEEE Military Communications Conference, MILCOM'08},
 doi          = {10.1109/MILCOM.2008.4753614},
)
@incollection(uppaal04,
 author       = {G. Behrmann and A. David and K. G. Larsen},
 year         = {2004},
 title        = {{A Tutorial on \textsc{Uppaal}}},
 editor       = {Marco Bernardo and Flavio Corradini},
 booktitle    = {Formal Methods for the Design of Real-Time Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {3185},
 publisher    = {Springer},
 pages        = {200--236},
 doi          = {10.1007/978-3-540-30080-9\_7},
)
@article(BOG02,
 author       = {Karthikeyan Bhargavan and Davor Obradovic and Carl A. Gunter},
 year         = {2002},
 title        = {Formal Verification of Standards for Distance Vector Routing Protocols},
 journal      = {J. ACM},
 volume       = {49},
 number       = {4},
 pages        = {538--576},
 doi          = {10.1145/581771.581775},
)
@article(Blanchet16,
 author       = {B. Blanchet},
 year         = {2016},
 title        = {Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif},
 journal      = {Foundations and Trends in Privacy and Security},
 volume       = {1},
 number       = {1-2},
 pages        = {1--135},
 doi          = {10.1561/3300000004},
)
@inproceedings(ESOP16,
 author       = {E. Bres and R. van Glabbeek and P. H\"{o}fner},
 year         = {2016},
 title        = {A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract)},
 editor       = {P. Thiemann},
 booktitle    = {Programming Languages and Systems (ESOP'16)},
 series       = {Lecture Notes in Computer Science},
 volume       = {9632},
 publisher    = {Springer},
 pages        = {95--122},
 doi          = {10.1007/978-3-662-49498-1\_5},
)
@inproceedings(CBMC,
 author       = {E. Clarke and D. Kroening and F. Lerda},
 year         = {2004},
 title        = {A Tool for Checking {ANSI-C} Programs},
 editor       = {K. Jensen and A. Podelski},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04)},
 series       = {Lecture Notes in Computer Science},
 volume       = {2988},
 publisher    = {Springer},
 pages        = {168--176},
 doi          = {10.1007/978-3-540-24730-2\_15},
)
@misc(rfc5340,
 author       = {R. Coltun and D. Ferguson and J. Moy and A. Lindem},
 year         = {2008},
 title        = {{OSPF for IPv6}},
 howpublished = {RFC 5340, Network Working Group},
 url          = {http://www.ietf.org/rfc/rfc5340.txt},
)
@inproceedings(Z3,
 author       = {De Moura, L. and Bj{\o}rner, N.},
 year         = {2008},
 title        = {{Z3:} An Efficient {SMT} Solver},
 editor       = {C. R. Ramakrishnan and J. Rehof},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08)},
 series       = {Lecture Notes in Computer Science},
 volume       = {4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@article(Dijkstra59,
 author       = {E. W. Dijkstra},
 year         = {1959},
 title        = {A Note on Two Problems in Connexion with Graphs},
 journal      = {Numerische Mathematik},
 volume       = {1},
 number       = {1},
 pages        = {269--271},
 doi          = {10.1007/BF01386390},
)
@inproceedings(DHW20,
 author       = {J. Drury and P. H\"ofner and W. Wang},
 year         = {2020},
 title        = {Formal Models of the {OSPF} Routing Protocol},
 editor       = {A. Fehnker and H. Garavel},
 booktitle    = {Models for Formal Analysis of Real Systems (MARS'20)},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {316},
 publisher    = {Open Publishing Association},
 pages        = {72--120},
 doi          = {10.4204/EPTCS.316.4},
)
@incollection(Emerson91,
 author       = {E. A. Emerson},
 year         = {1990},
 title        = {Temporal and Modal Logic},
 booktitle    = {Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics},
 publisher    = {MIT Press},
 pages        = {995--1072},
 doi          = {10.1016/B978-0-444-88074-1.50021-4},
)
@conference(TACAS12,
 author       = {A. Fehnker and R. J. van Glabbeek and P H{\"o}fner and A. K. McIver and M. Portmann and W. L. Tan},
 year         = {2012},
 title        = {Automated Analysis of {AODV} using {UPPAAL}},
 editor       = {C. Flanagan and B. K{\"onig}},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems {(TACAS '12)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {7214},
 publisher    = {Springer},
 pages        = {173--187},
 doi          = {10.1007/978-3-642-28756-5\_13},
)
@inproceedings(FHM07,
 author       = {A. Fehnker and L. van Hoesel and A. Mader},
 year         = {2007},
 title        = {Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks},
 booktitle    = {Integrated Formal Methods, IFM'07},
 series       = {Lecture Notes in Computer Science},
 volume       = {4591},
 publisher    = {Springer},
 pages        = {253--272},
 doi          = {10.1007/978-3-540-73210-5\_14},
)
@inproceedings(MSWIM13,
 author       = {R. J. van Glabbeek and P. H{\"o}fner and W. L. Tan and M. Portmann},
 year         = {2013},
 title        = {Sequence Numbers Do Not Guarantee Loop Freedom ---{AODV} Can Yield Routing Loops---},
 booktitle    = {Modeling, Analysis and Simulation of Wireless and Mobile Systems {(MSWiM '13)}},
 publisher    = {ACM},
 pages        = {91--100},
 doi          = {10.1145/2507924.2507943},
)
@inproceedings(HLS99,
 author       = {K. Havelund and K. G. Larsen and A. Skou},
 year         = {1999},
 title        = {Formal Verification of a Power Controller Using the Real-Time Model Checker {\sc Uppaal}\xspace},
 editor       = {J.-P. Katoen},
 booktitle    = {Formal Methods for Real-Time and Probabilistic Systems (ARTS'99)},
 series       = {Lecture Notes in Computer Science},
 volume       = {1601},
 publisher    = {Springer},
 pages        = {277--298},
 doi          = {10.1007/3-540-48778-6\_17},
)
@misc(IEEE80211,
 author       = {{ISO/IEC/IEEE 8802-11}},
 year         = {2018},
 title        = {Information Technology --- Telecommunications and information exchange between systems --- Local and metropolitan area networks --- Specific requirements --- Part 11: Wireless {LAN} Medium Access Control {(MAC)} and Physical Layer {(PHY)} specifications},
 url          = {https://www.iso.org/standard/73367.html},
)
@misc(JonesLeMoigne06,
 author       = {E. Jones and Le Moigne, O.},
 year         = {2006},
 title        = {{OSPF} Security Vulnerabilities Analysis},
 howpublished = {Routing Protocol Security},
 url          = {https://tools.ietf.org/id/draft-ietf-rpsec-ospf-vuln-02.txt},
)
@article(LPY97,
 author       = {K. G. Larsen and P. Pettersson and {Wang Yi}},
 year         = {1997},
 title        = {{UPPAAL} in a Nutshell},
 journal      = {International Journal of Software Tools for Technology Transfer},
 volume       = {1},
 number       = {1-2},
 pages        = {134--152},
 doi          = {10.1007/s100090050010},
)
@misc(Malik,
 author       = {S.U.R Malik and S. K. Srinivasan and S. U. Khan},
 year         = {2012},
 title        = {A Methodology for {OSPF} Routing Protocol Verification},
)
@inproceedings(MSCB13,
 author       = {S. Meier and B. Schmidt and C. Cremers and D. Basin},
 year         = {2013},
 title        = {The {TAMARIN} Prover for the Symbolic Analysis of Security Protocols},
 editor       = {N. Sharygina and H. Veith},
 booktitle    = {Computer Aided Verification {(CAV'13)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8044},
 publisher    = {Springer},
 pages        = {696--701},
 doi          = {10.1007/978-3-642-39799-8\_48},
)
@inproceedings(MK10,
 author       = {S. Miskovic and E. W. Knightly},
 year         = {2010},
 title        = {Routing Primitives for Wireless Mesh Networks: Design, Analysis and Experiments},
 booktitle    = {INFOCOM'10},
 publisher    = {IEEE},
 pages        = {2793--2801},
 doi          = {10.1109/INFCOM.2010.5462111},
)
@misc(rfc2328,
 author       = {J. Moy},
 year         = {1998},
 title        = {{OSPF Version 2}},
 howpublished = {RFC 2328, Network Working Group},
 url          = {http://www.ietf.org/rfc/rfc2328.txt},
)
@misc(NKGB12,
 author       = {G. Nakibly and D. Gonikman and A. Kirshon and D. Boneh},
 year         = {2012},
 title        = {Persistent {OSPF} Attacks},
)
@inproceedings(NakiblyEtAl14,
 author       = {G. Nakibly and A. Sosnovich and E. Menahem and A. Waizel and Y. Elovici},
 year         = {2014},
 title        = {{OSPF} Vulnerability to Persistent Poisoning Attacks: A Systematic Analysis},
 booktitle    = {Computer Security Applications Conference},
 series       = {ACSAC '14},
 publisher    = {ACM},
 pages        = {336--345},
 doi          = {10.1145/2664243.2664278},
)
@inproceedings(RA04,
 author       = {R. de Renesse and A.H. Aghvami},
 year         = {2004},
 title        = {Formal Verification of Ad Hoc Routing Protocols Using {SPIN} Model Checker},
 booktitle    = {IEEE MELECON'04},
 publisher    = {IEEE},
 pages        = {1177 -- 1182},
 doi          = {10.1109/MELCON.2004.1348275},
)
@inproceedings(WPP04,
 author       = {O. Wibling and J. Parrow and A. N. Pears},
 year         = {2004},
 title        = {Automatized Verification of Ad Hoc Routing Protocols},
 booktitle    = {Formal Techniques for Networked and Distributed Systems, FORTE'04},
 series       = {Lecture Notes in Computer Science},
 volume       = {3235},
 publisher    = {Springer},
 pages        = {343--358},
 doi          = {10.1007/978-3-540-30232-2\_22},
)