@book(abrialmodeling2010,
 author       = {Jean-Raymond Abrial},
 year         = {2010},
 title        = {{Modeling in Event-B}},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139195881},
)
@article(abrial2010rodin,
 author       = {Jean-Raymond Abrial and Michael Butler and Stefan Hallerstede and Thai Son Hoang and Farhad Mehta and Laurent Voisin},
 year         = {2010},
 title        = {Rodin: an open toolset for modelling and reasoning in {Event-B}},
 journal      = {International Journal on Software Tools for Technology Transfer},
 volume       = {12},
 number       = {6},
 pages        = {447--466},
 doi          = {10.1007/s10009-010-0145-y},
)
@book(bertot2013interactive,
 author       = {Yves Bertot and Pierre Cast{\'e}ran},
 year         = {2013},
 title        = {Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-07964-5},
)
@article(Bogue:11,
 author       = {Robert Bogue},
 year         = {2011},
 title        = {Robots in the nuclear industry: a review of technologies and applications},
 journal      = {Industrial Robot: An International Journal},
 volume       = {38},
 number       = {2},
 pages        = {113--118},
 doi          = {10.1108/01439911111106327},
)
@article(Broy18,
 author       = {Manfred Broy},
 year         = {2018},
 title        = {A logical approach to systems engineering artifacts: semantic relationships and dependencies beyond traceability -- from requirements to functional and architectural views},
 journal      = {Software and System Modeling},
 volume       = {17},
 number       = {2},
 pages        = {365--393},
 doi          = {10.1007/s10270-017-0619-4},
)
@article(Broy18b,
 author       = {Manfred Broy},
 year         = {2018},
 title        = {Theory and methodology of assumption/commitment based system interface specification and architectural contracts},
 journal      = {Formal Methods in System Design},
 volume       = {52},
 number       = {1},
 pages        = {33--87},
 doi          = {10.1007/s10703-017-0304-9},
)
@inproceedings(champion2016cocospec,
 author       = {Adrien Champion and Arie Gurfinkel and Temesghen Kahsai and Cesare Tinelli},
 year         = {2016},
 title        = {CoCoSpec: A mode-aware contract language for reactive systems},
 booktitle    = {International Conference on Software Engineering and Formal Methods},
 series       = {LNCS},
 volume       = {9763},
 organization = {Springer},
 pages        = {347--366},
 doi          = {10.1007/978-3-319-41591-8_24},
)
@inproceedings(cimatti2013ocra,
 author       = {Alessandro Cimatti and Michele Dorigatti and Stefano Tonetta},
 year         = {2013},
 title        = {OCRA: A tool for checking the refinement of temporal contracts},
 booktitle    = {International Conference on Automated Software Engineering (ASE)},
 organization = {IEEE},
 pages        = {702--705},
 doi          = {10.1109/ASE.2013.6693137},
)
@book(clarke1999model,
 author       = {Edmund M Clarke and Orna Grumberg and Doron Peled},
 year         = {1999},
 title        = {Model checking},
 publisher    = {MIT press},
)
@inproceedings(cofer2012compositional,
 author       = {Darren Cofer and Andrew Gacek and Steven Miller and Michael W Whalen and Brian LaValley and Lui Sha},
 year         = {2012},
 title        = {Compositional verification of architectural models},
 booktitle    = {NASA Formal Methods Symposium},
 series       = {LNCS},
 volume       = {7226},
 organization = {Springer},
 pages        = {126--140},
 doi          = {10.1007/978-3-642-13464-7_5},
)
@article(Dennis2012,
 author       = {Louise A. Dennis and Michael Fisher and Matthew P. Webster and Rafael H. Bordini},
 year         = {2012},
 title        = {Model checking agent programming languages},
 journal      = {Automated Software Engineering},
 volume       = {19},
 number       = {1},
 pages        = {5--63},
 doi          = {10.1007/s10515-011-0088-x},
)
@inproceedings(DRONA,
 author       = {Ankush Desai and Shaz Qadeer and Sanjit A. Seshia},
 year         = {2018},
 title        = {Programming Safe Robotics Systems: Challenges and Advances},
 editor       = {Tiziana Margaria and Bernhard Steffen},
 booktitle    = {Leveraging Applications of Formal Methods, Verification and Validation. Verification},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {103--119},
 doi          = {10.1007/978-3-030-03421-4_8},
)
@article(dijkstra1975guarded,
 author       = {Edsger W Dijkstra},
 year         = {1975},
 title        = {Guarded commands, nondeterminacy and formal derivation of programs},
 journal      = {Communications of the ACM},
 volume       = {18},
 number       = {8},
 pages        = {453--457},
 doi          = {10.1145/360933.360975},
)
@inproceedings(Farrell2018,
 author       = {Marie Farrell and Matt Luckcuck and Michael Fisher},
 year         = {2018},
 title        = {{Robotics and Integrated Formal Methods: Necessity meets Opportunity}},
 booktitle    = {Integrated Formal Methods},
 series       = {LNCS},
 volume       = {11023},
 publisher    = {Springer},
 pages        = {161--171},
 doi          = {10.1007/978-3-319-98938-9_10},
)
@inproceedings(farrell2017specification,
 author       = {Marie Farrell and Rosemary Monahan and James F Power},
 year         = {2017},
 title        = {Specification Clones: An Empirical Study of the Structure of Event-B Specifications},
 booktitle    = {International Conference on Software Engineering and Formal Methods},
 series       = {LNCS},
 volume       = {10469},
 organization = {Springer},
 pages        = {152--167},
 doi          = {10.1007/978-3-319-66197-1_10},
)
@article(Hastie18,
 author       = {Helen F. Hastie and Katrin Solveig Lohan and Mike J. Chantler and David A. Robb and Subramanian Ramamoorthy and Ronald P. A. Petrick and Sethu Vijayakumar and David Lane},
 year         = {2018},
 title        = {The {ORCA} Hub: Explainable Offshore Robotics through Intelligent Interfaces},
 journal      = {CoRR},
 volume       = {abs/1803.02100},
 url          = {http://arxiv.org/abs/1803.02100},
)
@article(hoare1969axiomatic,
 author       = {C. A. R. Hoare},
 year         = {1969},
 title        = {An axiomatic basis for computer programming},
 journal      = {Communications of the ACM},
 volume       = {12},
 number       = {10},
 pages        = {576--580},
 doi          = {10.1145/363235.363259},
)
@article(Hoare1978,
 author       = {C. A. R. Hoare},
 year         = {1978},
 title        = {{Communicating sequential processes}},
 journal      = {Communications of the ACM},
 volume       = {21},
 number       = {8},
 pages        = {666--677},
 doi          = {10.1145/359576.359585},
)
@article(Jones83,
 author       = {Cliff B. Jones},
 year         = {1983},
 title        = {{Tentative Steps Toward a Development Method for Interfering Programs}},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {5},
 number       = {4},
 pages        = {596--619},
 doi          = {10.1145/69575.69577},
)
@article(Luckcuck2019,
 author       = {Matt Luckcuck and Marie Farrell and Louise A. Dennis and Clare Dixon and Michael Fisher},
 year         = {2019},
 title        = {{Formal Specification and Verification of Autonomous Robotic Systems: A Survey}},
 journal      = {ACM Comput. Surv.},
 volume       = {52},
 number       = {5},
 pages        = {1--41},
 doi          = {10.1145/3342355},
)
@inproceedings(LuckenederK18,
 author       = {Christoph Luckeneder and Hermann Kaindl},
 year         = {2018},
 title        = {{Systematic top-down design of cyber-physical models with integrated validation and formal verification}},
 booktitle    = {International Conference on Software Engineering},
 pages        = {274--275},
 doi          = {10.1145/3183440.3194967},
)
@article(menghi2019specification,
 author       = {Claudio Menghi and Christos Tsigkanos and Patrizio Pelliccione and Carlo Ghezzi and Thorsten Berger},
 year         = {2019},
 title        = {Specification patterns for robotic missions},
 journal      = {IEEE Transactions on Software Engineering},
 doi          = {10.1109/TSE.2019.2945329},
)
@book(morganrefinement1988,
 author       = {Carroll Morgan and Ken Robinson and Paul Gardiner},
 year         = {1988},
 title        = {On the {Refinement} {Calculus}},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4471-3273-8},
)
@book(mosses2004casl,
 author       = {Peter D Mosses},
 year         = {2004},
 title        = {CASL reference manual: The complete documentation of the common algebraic specification language},
 publisher    = {Springer},
 doi          = {10.1007/b96103},
)
@inproceedings(Pnueli77temporal,
 author       = {A. Pnueli},
 year         = {1977},
 title        = {{The Temporal Logic of Programs}},
 booktitle    = {18th Symposium on the Foundations of Computer Science},
 publisher    = {IEEE},
 pages        = {46--57},
 doi          = {10.1109/SFCS.1977.32},
)
@inproceedings(Shakhimardanov2010,
 author       = {Azamat Shakhimardanov and Nico Hochgeschwender and Gerhard Kraetzschmar},
 year         = {2010},
 title        = {{Component models in robotics software}},
 booktitle    = {Workshop on Performance Metrics for Intelligent Systems},
 publisher    = {ACM},
 pages        = {82--87},
 doi          = {10.1145/2377576.2377592},
)
@article(Spellini2019,
 author       = {Stefano Spellini and Michele Lora and Franco Fummi and Sudipta Chattopadhyay},
 year         = {2019},
 title        = {Compositional Design of Multi-Robot Systems Control Software on ROS},
 journal      = {ACM Trans. Embed. Comput. Syst.},
 volume       = {18},
 number       = {5s},
 doi          = {10.1145/3358197},
)
@book(spivey1988understanding,
 author       = {J Michael Spivey},
 year         = {1988},
 title        = {Understanding Z: a specification language and its formal semantics},
 publisher    = {Cambridge University Press},
)
@inproceedings(SIMPAL,
 author       = {Lucas Wagner and David Greve and Andrew Gacek},
 year         = {2017},
 title        = {SIMPAL: A Compositional Reasoning Framework for Imperative Programs},
 booktitle    = {Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software},
 series       = {SPIN 2017},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {90–93},
 doi          = {10.1145/3092282.3092290},
)
@article(WWADEMP19,
 author       = {Matt Webster and David Western and Araiza-Illan, Dejanira and Clare Dixon and Kerstin Eder and Michael Fisher and Anthony G Pipe},
 year         = {2020},
 title        = {A corroborative approach to verification and validation of human–robot teams},
 journal      = {The International Journal of Robotics Research},
 volume       = {39},
 number       = {1},
 pages        = {73--99},
 doi          = {10.1177/0278364919883338},
)
@article(Wilcox:92,
 author       = {Brian H. Wilcox},
 year         = {1992},
 title        = {Robotic vehicles for planetary exploration},
 journal      = {Applied Intelligence},
 volume       = {2},
 number       = {2},
 pages        = {181--193},
 doi          = {10.1007/BF00058762},
)