@inproceedings(al2007simple,
 author       = {Al Hanbali, Ahmad and Arzad A Kherani and Philippe Nain},
 year         = {2007},
 title        = {{Simple Models for the Performance Evaluation of a Class of Two-Hop Relay Protocols}},
 booktitle    = {International Conference on Research in Networking},
 organization = {Springer},
 pages        = {191--202},
 doi          = {10.1007/978-3-540-72606-7_17},
)
@misc(athena1,
 author       = {Konstantine Arkoudas},
 title        = {{{A}thena}},
 url          = {http://proofcentral.org/athena},
)
@article(arkoudas2005simplifying,
 author       = {Konstantine Arkoudas},
 year         = {2005},
 title        = {{Simplifying Proofs in Fitch-Style Natural Deduction Systems}},
 journal      = {Journal of Automated Reasoning},
 volume       = {34},
 number       = {3},
 pages        = {239--294},
 doi          = {10.1007/s10817-005-9000-3},
)
@book(arkoudas2017fundamental,
 author       = {Konstantine Arkoudas and David Musser},
 year         = {2017},
 title        = {{Fundamental Proof Methods in Computer Science: A Computer-Based Approach}},
 publisher    = {MIT Press},
 doi          = {10.1017/s1471068420000071},
)
@article(attiya2001time,
 author       = {Hagit Attiya and Djerassi-Shintel, Taly},
 year         = {2001},
 title        = {{Time Bounds for Decision Problems in the Presence of Timing Uncertainty and Failures}},
 journal      = {Journal of Parallel and Distributed Computing},
 volume       = {61},
 number       = {8},
 pages        = {1096--1109},
 doi          = {10.1006/jpdc.2001.1730},
)
@article(attiya1994bounds,
 author       = {Hagit Attiya and Cynthia Dwork and Nancy Lynch and Larry Stockmeyer},
 year         = {1994},
 title        = {{Bounds on the Time to Reach Agreement in the Presence of Timing Uncertainty}},
 journal      = {Journal of the ACM (JACM)},
 volume       = {41},
 number       = {1},
 pages        = {122--152},
 doi          = {10.21236/ada229766},
)
@inproceedings(balachandran2020decentralized,
 author       = {Swee Balachandran and Christopher Manderino and Mu{\~n}oz, C{\'e}sar and Mar{\'\i}a Consiglio},
 year         = {2020},
 title        = {{A Decentralized Framework to Support UAS Merging and Spacing Operations in Urban Canyons}},
 booktitle    = {2020 International Conference on Unmanned Aircraft Systems (ICUAS)},
 organization = {IEEE},
 pages        = {204--210},
 doi          = {10.1109/icuas48674.2020.9213973},
)
@inproceedings(berman1989towards,
 author       = {Piotr Berman and Juan A Garay and Kenneth J Perry},
 year         = {1989},
 title        = {{Towards Optimal Distributed Consensus}},
 booktitle    = {FOCS},
 volume       = {89},
 pages        = {410--415},
 doi          = {10.1109/sfcs.1989.63511},
)
@book(bertsekas1992data,
 author       = {Dimitri P Bertsekas and Robert G Gallager and Pierre Humblet},
 year         = {1992},
 title        = {{Data Networks}},
 volume       = {2},
 publisher    = {Prentice-Hall International New Jersey},
)
@inproceedings(brittain2018autonomous,
 author       = {Marc Brittain and Peng Wei},
 year         = {2018},
 title        = {{Autonomous Aircraft Sequencing and Separation with Hierarchical Deep Reinforcement Learning}},
 booktitle    = {Proceedings of the International Conference for Research in Air Transportation},
)
@article(cao2018airborne,
 author       = {Xianbin Cao and Peng Yang and Mohamed Alzenad and Xing Xi and Dapeng Wu and Halim Yanikomeroglu},
 year         = {2018},
 title        = {{Airborne Communication Networks: A Survey}},
 journal      = {{IEEE Journal on Selected Areas in Communications}},
 volume       = {36},
 number       = {9},
 pages        = {1907--1926},
 doi          = {10.1109/jsac.2018.2864423},
)
@mastersthesis(chaouch2015formalization,
 author       = {Donia Chaouch},
 year         = {2015},
 title        = {Formalization of Continuous Time Markov Chains with Applications in Queueing Theory},
 school       = {Concordia University},
)
@article(charron2009heard,
 author       = {Charron-Bost, Bernadette and Andr{\'e} Schiper},
 year         = {2009},
 title        = {{The Heard-Of Model: Computing in Distributed Systems With Benign Faults}},
 journal      = {Distributed Computing},
 volume       = {22},
 number       = {1},
 pages        = {49--71},
 doi          = {10.1007/s00446-009-0084-6},
)
@inproceedings(darema2004dynamic,
 author       = {Frederica Darema},
 year         = {2004},
 title        = {{Dynamic Data-Driven Application Systems: A New Paradigm for Application Simulations and Measurements}},
 booktitle    = {Computational Science-ICCS 2004},
 organization = {Springer},
 pages        = {662--669},
 doi          = {10.1007/978-3-540-24688-6_86},
)
@article(debrat2012verifying,
 author       = {Henri Debrat and Stephan Merz},
 year         = {2012},
 title        = {{Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model}},
 journal      = {Archive of Formal Proofs},
 volume       = {2012},
)
@article(delporte2007perfectly,
 author       = {Delporte-Gallet, Carole and Hugues Fauconnier and Rachid Guerraoui and Bastian Pochon},
 year         = {2007},
 title        = {{The Perfectly Synchronized Round-Based Model of Distributed Computing}},
 journal      = {Information and Computation},
 volume       = {205},
 number       = {5},
 pages        = {783--815},
 doi          = {10.1016/j.ic.2006.11.003},
)
@inproceedings(druagoi2016psync,
 author       = {Dr{\u{a}}goi, Cezara and Thomas A Henzinger and Damien Zufferey},
 year         = {2016},
 title        = {{PSync: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms}},
 booktitle    = {ACM SIGPLAN Notices},
 volume       = {51},
 organization = {ACM},
 pages        = {400--415},
 doi          = {10.1145/2837614.2837650},
)
@book(fagin2004reasoning,
 author       = {Ronald Fagin and Joseph Y Halpern and Yoram Moses and Moshe Vardi},
 year         = {2004},
 title        = {{Reasoning About Knowledge}},
 publisher    = {MIT press},
 doi          = {10.7551/mitpress/5803.001.0001},
)
@book(gallager2013stochastic,
 author       = {Robert G Gallager},
 year         = {2013},
 title        = {{Stochastic Processes: Theory for Applications}},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/cbo9781139626514},
)
@article(gonczy2007modeling,
 author       = {L{\'a}szl{\'o} G{\"o}nczy and M{\'a}t{\'e} Kov{\'a}cs and D{\'a}niel Varr{\'o}},
 year         = {2007},
 title        = {{Modeling and Verification of Reliable Messaging by Graph Transformation Systems}},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {175},
 number       = {4},
 pages        = {37--50},
 doi          = {10.1016/j.entcs.2007.04.015},
)
@incollection(gordon1989mechanizing,
 author       = {Michael JC Gordon},
 year         = {1989},
 title        = {{Mechanizing Programming Logics in Higher Order Logic}},
 booktitle    = {Current trends in hardware verification and automated theorem proving},
 publisher    = {Springer},
 pages        = {387--439},
 doi          = {10.1007/978-1-4612-3658-0_10},
)
@article(grossglauser2002mobility,
 author       = {Matthias Grossglauser and David NC Tse},
 year         = {2002},
 title        = {{Mobility Increases the Capacity of Ad Hoc Wireless Networks}},
 journal      = {IEEE/ACM transactions on networking},
 volume       = {10},
 number       = {4},
 pages        = {477--486},
 doi          = {10.1109/tnet.2002.801403},
)
@inproceedings(hamdi2020review,
 author       = {Mustafa Maad Hamdi and Lukman Audah and Sami Abduljabbar Rashid and Alaa Hamid Mohammed and Sameer Alani and Ahmed Shamil Mustafa},
 year         = {2020},
 title        = {{A Review of Applications, Characteristics and Challenges in Vehicular Ad-Hoc Networks (VANETs)}},
 booktitle    = {2020 International Congress on Human-Computer Interaction, Optimization and Robotic Applications (HORA)},
 organization = {IEEE},
 pages        = {1--7},
 doi          = {10.1109/hora49412.2020.9152928},
)
@inproceedings(hasan2008probabilistic,
 author       = {Osman Hasan},
 year         = {2008},
 title        = {{Probabilistic Analysis Using Theorem Proving}},
 booktitle    = {21 st International Conference on Theorem Proving in Higher Order Logics},
 organization = {Citeseer},
 pages        = {21},
)
@article(hasan2006formalization,
 author       = {Osman Hasan and Sofi{\`e}ne Tahar},
 year         = {2007},
 title        = {{Formalization of the Standard Uniform random variable}},
 journal      = {Theoretical Computer Science},
 volume       = {382},
 pages        = {71--83},
 doi          = {10.1016/j.tcs.2007.05.009},
)
@article(hasan2008using,
 author       = {Osman Hasan and Sofi{\`e}ne Tahar},
 year         = {2008},
 title        = {{Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables}},
 journal      = {Journal of Automated Reasoning},
 volume       = {41},
 number       = {3-4},
 pages        = {295--323},
 doi          = {10.1007/s10817-008-9113-6},
)
@article(hasan2009formal,
 author       = {Osman Hasan and Sofiene Tahar},
 year         = {2009},
 title        = {{Formal Verification of Tail Distribution Bounds in the {HOL} Theorem Prover}},
 journal      = {Mathematical Methods in the Applied Sciences},
 volume       = {32},
 number       = {4},
 pages        = {480--504},
 doi          = {10.1002/mma.1055},
)
@inproceedings(hasan2010formal,
 author       = {Osman Hasan and Sofiene Tahar},
 year         = {2010},
 title        = {{Formal Probabilistic Analysis: A Higher-Order Logic Based Approach}},
 booktitle    = {International Conference on Abstract State Machines, Alloy, B and Z},
 organization = {Springer},
 pages        = {2--19},
 doi          = {10.1007/978-3-642-11811-1_2},
)
@article(hasan2011reasoning,
 author       = {Osman Hasan and Sofi{\`e}ne Tahar},
 year         = {2011},
 title        = {{Reasoning About Conditional Probabilities in a Higher-Order-Logic Theorem Prover}},
 journal      = {Journal of Applied Logic},
 volume       = {9},
 number       = {1},
 pages        = {23--40},
 doi          = {10.1016/j.jal.2011.01.001},
)
@inproceedings(hawblitzel2015ironfleet,
 author       = {Chris Hawblitzel and Jon Howell and Manos Kapritsos and Jacob R Lorch and Bryan Parno and Michael L Roberts and Srinath Setty and Brian Zill},
 year         = {2015},
 title        = {{IronFleet: Proving Practical Distributed Systems Correct}},
 booktitle    = {Proceedings of the 25th Symposium on Operating Systems Principles},
 organization = {ACM},
 pages        = {1--17},
 doi          = {10.1145/2815400.2815428},
)
@article(hawblitzel2017ironfleet,
 author       = {Chris Hawblitzel and Jon Howell and Manos Kapritsos and Jacob R Lorch and Bryan Parno and Michael L Roberts and Srinath Setty and Brian Zill},
 year         = {2017},
 title        = {{IronFleet: Proving Safety and Liveness of Practical Distributed Systems}},
 journal      = {Communications of the ACM},
 volume       = {60},
 number       = {7},
 pages        = {83--92},
 doi          = {10.1145/3068608},
)
@article(kushwah2020multipath,
 author       = {Rashmi Kushwah and Shashikala Tapaswi and Ajay Kumar},
 year         = {2020},
 title        = {{Multipath Delay Analysis Using Queuing Theory for Gateway Selection in Hybrid MANET}},
 journal      = {Wireless Personal Communications},
 volume       = {111},
 number       = {1},
 pages        = {9--32},
 doi          = {10.1007/s11277-019-06842-9},
)
@book(last2017lectures,
 author       = {G{\"u}nter Last and Mathew Penrose},
 year         = {2017},
 title        = {{Lectures on the Poisson Process}},
 volume       = {7},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/9781316104477.007},
)
@inproceedings(lee2013investigating,
 author       = {Seung Man Lee and Chunki Park and Marcus A Johnson and Eric R Mueller},
 year         = {2013},
 title        = {{Investigating Effects of Well Clear Definitions on UAS Sense-And-Avoid Operations in Enroute and Transition Airspace}},
 booktitle    = {2013 Aviation Technology, Integration, and Operations Conference},
 doi          = {10.2514/6.2013-4308},
)
@inproceedings(leino2010dafny,
 author       = {K. Rustan M. Leino},
 year         = {2010},
 title        = {{Dafny: An Automatic Program Verifier for Functional Correctness}},
 booktitle    = {International Conference on Logic for Programming Artificial Intelligence and Reasoning},
 organization = {Springer},
 pages        = {348--370},
 doi          = {10.1007/978-3-642-17511-4_20},
)
@book(leon-garcia_probability_1994,
 author       = {Leon-Garcia, Alberto},
 year         = {1994},
 title        = {{Probability and Random Processes for Electrical Engineering}},
 edition      = {2nd},
 publisher    = {Addison-Wesley},
 address      = {{Reading, MA}},
)
@article(lipsky2009,
 author       = {Lester Lipsky},
 year         = {2009},
 title        = {{M/M/1 Queue}},
 journal      = {{Queueing Theory: A Linear Algebraic Approach}},
 pages        = {33--75},
 doi          = {10.1007/978-0-387-49706-8_2},
)
@article(little1961proof,
 author       = {John DC Little},
 year         = {1961},
 title        = {{A Proof for the Queuing Formula: L= $\lambda$ W}},
 journal      = {Operations research},
 volume       = {9},
 number       = {3},
 pages        = {383--387},
 doi          = {10.1287/opre.9.3.383},
)
@article(liu2013delivery,
 author       = {Jiajia Liu and Xiaohong Jiang and Hiroki Nishiyama and Nei Kato},
 year         = {2013},
 title        = {{On the Delivery Probability of Two-Hop Relay MANETs with Erasure Coding}},
 journal      = {IEEE Transactions on Communications},
 volume       = {61},
 number       = {4},
 pages        = {1314--1326},
 doi          = {10.1109/tcomm.2013.020413.120198},
)
@article(luckner2004hazard,
 author       = {Robert Luckner and Gordon H{\"o}hne and Michael Fuhrmann},
 year         = {2004},
 title        = {{Hazard Criteria for Wake Vortex Encounters During Approach}},
 journal      = {Aerospace Science and Technology},
 volume       = {8},
 number       = {8},
 pages        = {673--687},
 doi          = {10.1016/j.ast.2004.06.008},
)
@techreport(malkhi2008stoppable,
 author       = {Dahlia Malkhi and Leslie Lamport and Lidong Zhou},
 year         = {2008},
 title        = {{Stoppable Paxos}},
 type         = {Technical Report},
 institution  = {Microsoft Research},
)
@book(manzano1996extensions,
 author       = {Maria Manzano},
 year         = {1996},
 title        = {{Extensions of First-Order Logic}},
 publisher    = {Cambridge University Press},
)
@inproceedings(mcmillan2018deductive,
 author       = {Kenneth L McMillan and Oded Padon},
 year         = {2018},
 title        = {{Deductive Verification in Decidable Fragments with Ivy}},
 booktitle    = {Static Analysis},
 organization = {Springer},
 pages        = {43--55},
 doi          = {10.1007/978-3-319-99725-4_4},
)
@inbook(meester_slooten_2021,
 author       = {Ronald Meester and Klaas Slooten},
 year         = {2021},
 title        = {Some Philosophy of Probability, Statistics, and Forensic Science},
 pages        = {1\IeC{\textendash}29},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/9781108596176.002},
)
@inproceedings(mhamdi2010formalizationlebesque,
 author       = {Tarek Mhamdi and Osman Hasan and Sofi{\`e}ne Tahar},
 year         = {2010},
 title        = {{On the Formalization of the Lebesgue Integration Theory in HOL}},
 booktitle    = {International Conference on Interactive Theorem Proving},
 organization = {Springer},
 pages        = {387--402},
 doi          = {10.1007/978-3-642-14052-5_27},
)
@article(mhamdi2013formalizationmeasure,
 author       = {Tarek Mhamdi and Osman Hasan and Sofi\`{e}ne Tahar},
 year         = {2013},
 title        = {{Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL}},
 journal      = {ACM Transactions on Embedded Computing Systems},
 volume       = {12},
 number       = {1},
 doi          = {10.1145/2406336.2406349},
)
@article(molisch2009survey,
 author       = {Andreas F Molisch and Fredrik Tufvesson and Johan Karedal and Christoph F Mecklenbrauker},
 year         = {2009},
 title        = {{A Survey on Vehicle-to-Vehicle Propagation Channels}},
 journal      = {IEEE Wireless Communications},
 volume       = {16},
 number       = {6},
 pages        = {12--22},
 doi          = {10.1109/mwc.2009.5361174},
)
@inproceedings(musser-varela-agere-2013,
 author       = {David R. Musser and Carlos A. Varela},
 year         = {2013},
 title        = {{Structured Reasoning About Actor Systems}},
 booktitle    = {Proceedings of the 2013 Workshop on Programming Based on Actors, Agents, and Decentralized Control},
 series       = {AGERE!},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {37--48},
 doi          = {10.1145/2541329.2541334},
)
@article(padon2016ivy,
 author       = {Oded Padon and Kenneth L McMillan and Aurojit Panda and Mooly Sagiv and Sharon Shoham},
 year         = {2016},
 title        = {{Ivy: Safety Verification by Interactive Generalization}},
 journal      = {ACM SIGPLAN Notices},
 volume       = {51},
 number       = {6},
 pages        = {614--630},
 doi          = {10.1145/2980983.2908118},
)
@inproceedings(paul-nfm-2021,
 author       = {Saswata Paul and Gul A. Agha and Stacy Patterson and Carlos A. Varela},
 year         = {2021},
 title        = {{Verification of Eventual Consensus in Synod using a Failure-Aware Actor Model}},
 booktitle    = {Proceedings of the 13th NASA Formal Methods Symposium (NFM 2021)},
 pages        = {249--267},
 doi          = {10.1007/978-3-030-76384-8_16},
)
@inproceedings(paul-dddas-2020,
 author       = {Saswata Paul and Fotis Kopsaftopoulos and Stacy Patterson and Carlos A. Varela},
 year         = {2020},
 title        = {{Dynamic Data-Driven Formal Progress Envelopes for Distributed Algorithms}},
 booktitle    = {Dynamic Data-Driven Application Systems},
 pages        = {245--252},
 doi          = {10.1007/978-3-030-61725-7_29},
)
@inproceedings(paul-dasc-2019,
 author       = {Saswata Paul and Stacy Patterson and Carlos A. Varela},
 year         = {2019},
 title        = {{Conflict-Aware Flight Planning for Avoiding Near Mid-Air Collisions}},
 booktitle    = {The 38th AIAA/IEEE Digital Avionics Systems Conference},
 address      = {San Diego, CA},
 pages        = {1--10},
 doi          = {10.1109/dasc43569.2019.9081658},
)
@inproceedings(paul-dasc-2020,
 author       = {Saswata Paul and Stacy Patterson and Carlos A. Varela},
 year         = {2020},
 title        = {{Collaborative Situational Awareness for Conflict-Aware Flight Planning}},
 booktitle    = {The 39th IEEE/AIAA Digital Avionics Systems Conference},
 pages        = {1--10},
 doi          = {10.1109/dasc50938.2020.9256620},
)
@mastersthesis(qasim2016formalization,
 author       = {Muhammad Qasim},
 year         = {2016},
 title        = {{Formalization of Normal Random Variables}},
 school       = {Concordia University},
 doi          = {10.1016/j.entcs.2013.09.001},
)
@article(wang2012cooperation,
 author       = {Xinbing Wang and Qiuyu Peng and Yingzhe Li},
 year         = {2012},
 title        = {{Cooperation Achieves Optimal Multicast Capacity-Delay Scaling in MANET}},
 journal      = {IEEE Transactions on Communications},
 volume       = {60},
 number       = {10},
 pages        = {3023--3031},
 doi          = {10.1109/tcomm.2012.081512.110535},
)
@inproceedings(wang2006fundamental,
 author       = {Yang Wang and Yiyuan J Zhao},
 year         = {2006},
 title        = {{Fundamental Issues in Systematic Design of Airborne Networks for Aviation}},
 booktitle    = {2006 IEEE Aerospace Conference},
 organization = {IEEE},
 pages        = {8--pp},
 doi          = {10.1109/aero.2006.1655882},
)
@inproceedings(wen2011analysis,
 author       = {Wen-jie, Xia and Yan Han and Feng-yu, Liu},
 year         = {2011},
 title        = {{The Analysis of M/M/1 Queue Model with N Policy for Damaged Nodes in MANET}},
 booktitle    = {2011 IEEE International Conference on Computer Science and Automation Engineering},
 volume       = {1},
 organization = {IEEE},
 pages        = {289--294},
 doi          = {10.1109/csae.2011.5953224},
)
@article(wing2011,
 author       = {David Wing and William Cotton},
 year         = {2011},
 title        = {{For Spacious Skies: Self-Separation with "Autonomous Flight Rules" in US Domestic Airspace}},
 doi          = {10.2514/6.2011-6865},
)
@article(woodcock2009formal,
 author       = {Jim Woodcock and Peter Gorm Larsen and Juan Bicarregui and John Fitzgerald},
 year         = {2009},
 title        = {{Formal Methods: Practice and Experience}},
 journal      = {ACM Computing Surveys},
 volume       = {41},
 number       = {4},
 pages        = {1--36},
 doi          = {10.5555/3065491.3065655},
)
@inproceedings(yin2004malb,
 author       = {Shouyi Yin and Xiaokang Lin},
 year         = {2004},
 title        = {{MALB: MANET Adaptive Load Balancing}},
 booktitle    = {IEEE 60th Vehicular Technology Conference, 2004},
 volume       = {4},
 organization = {IEEE},
 pages        = {2843--2847},
 doi          = {10.1109/vetecf.2004.1400578},
)