D. Althoff, J. Kuffner, D. Wollherr, and M. Buss, Safety assessment of robot trajectories for navigation in uncertain and dynamic environments, Autonomous Robots, vol.10, issue.2, pp.285-302, 2012.
DOI : 10.1109/TITS.2009.2020208

B. Bohrer, V. Rahli, I. Vukotic, M. Völp, and A. Platzer, Formally verified differential dynamic logic, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp.208-221, 2017.
DOI : 10.1145/2854065.2854077

F. Bonin-font, A. Ortiz, and G. Oliver, Visual Navigation for Mobile Robots: A Survey, Journal of Intelligent and Robotic Systems, vol.27, issue.1, pp.263-296, 2008.
DOI : 10.1243/0954410042794966

S. Bouraine, T. Fraichard, and H. Salhi, Provably safe navigation for mobile robots with limited field-of-views in dynamic environments, Autonomous Robots, vol.32, issue.3, pp.267-283, 2012.
DOI : 10.1177/0278364908097581

URL : https://hal.archives-ouvertes.fr/hal-00733913

T. Bräunl, Driving robots In: Embedded Robotics: Mobile Robot Design and Applications with Embedded Systems, pp.97-111, 2006.

O. Brock and O. Khatib, High-speed navigation using the global dynamic window approach, Proceedings 1999 IEEE International Conference on Robotics and Automation (Cat. No.99CH36288C), 1999.
DOI : 10.1109/ROBOT.1999.770002

H. Choset, K. Lynch, S. Hutchinson, G. Kantor, W. Burgard et al., Principles Of Robot Motion, 2005.

G. Collins, Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition In: Automata Theory and Formal Languages, 2nd GI Conference, pp.134-183, 1975.

J. Davenport and J. Heintz, Real quantifier elimination is doubly exponential, Journal of Symbolic Computation, vol.5, issue.1-2, pp.29-3510, 1988.
DOI : 10.1016/S0747-7171(88)80004-X

P. Fiorini and E. Prassler, Cleaning and household robots: A technology survey, 2000.

P. Fiorini and Z. Shiller, Motion Planning in Dynamic Environments Using Velocity Obstacles, The International Journal of Robotics Research, vol.3, issue.2, pp.760-772, 1998.
DOI : 10.1016/0954-1810(88)90025-8

D. Fox, W. Burgard, and S. Thrun, The dynamic window approach to collision avoidance, IEEE Robotics & Automation Magazine, vol.4, issue.1, pp.23-33, 1997.
DOI : 10.1109/100.580977

G. Frehse, C. Guernic, A. Donzé, S. Cotton, R. Ray et al., SpaceEx: Scalable Verification of Hybrid Systems, Computer Aided Verification - 23rd International Conference, CAV 2011. Proceedings, 2011.
DOI : 10.1007/978-3-642-00768-2_32

URL : https://hal.archives-ouvertes.fr/hal-00769608

N. Fulton, S. Mitsch, B. Bohrer, and A. Platzer, Bellerophon: Tactical Theorem Proving for??Hybrid Systems, LNCS, vol.35, issue.1, 2017.
DOI : 10.1007/978-3-642-38088-4_26

N. Fulton, S. Mitsch, J. Quesel, M. Völp, and A. Platzer, KeYmaera??X: An Axiomatic Tactical Theorem Prover for Hybrid Systems, LNCS, vol.9195, pp.527-538, 2015.
DOI : 10.1007/978-3-319-21401-6_36

P. Hart, N. Nilsson, and R. B. , A Formal Basis for the Heuristic Determination of Minimum Cost Paths, IEEE Transactions on Systems Science and Cybernetics, vol.4, issue.2, pp.100-107, 1968.
DOI : 10.1109/TSSC.1968.300136

S. Karaman and E. Frazzoli, Sampling-based algorithms for optimal motion planning with deterministic μ-calculus specifications, 2012 American Control Conference (ACC), pp.735-742, 2012.
DOI : 10.1109/ACC.2012.6315419

O. Khatib, Real-time obstacle avoidance for manipulators and mobile robots, Proceedings of the, pp.500-505, 1985.

H. Kress-gazit, G. Fainekos, and G. Pappas, Temporal-Logic-Based Reactive Mission and Motion Planning, IEEE Transactions on Robotics, vol.25, issue.6, pp.1370-1381, 2009.
DOI : 10.1109/TRO.2009.2030225

URL : http://www.public.asu.edu/~gfaineko/pub/tro2009.pdf

S. Loos, A. Platzer, and L. Nistor, Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified, LNCS, vol.38, pp.42-56, 2011.
DOI : 10.1007/3-540-64358-3_45

S. Loos, D. Renshaw, and A. Platzer, Formal verification of distributed aircraft controllers, Proceedings of the 16th international conference on Hybrid systems: computation and control, HSCC '13, pp.125-130, 2013.
DOI : 10.1145/2461328.2461350

S. Loos, D. Witmer, P. Steenkiste, and A. Platzer, Efficiency analysis of formally verified adaptive cruise controllers, 16th International IEEE Conference on Intelligent Transportation Systems (ITSC 2013), 2013.
DOI : 10.1109/ITSC.2013.6728453

K. Ma?ek, V. Govea, D. Fraichard, T. Siegwart, and R. , Towards Safe Vehicle Navigation in Dynamic Urban Scenarios, Automatika, vol.50, pp.3-4, 2009.

J. Minguez, L. Montano, S. , and J. , Abstracting Vehicle Shape and Kinematic Constraints from Obstacle Avoidance Methods, Autonomous Robots, vol.15, issue.5, 2006.
DOI : 10.1007/s10514-006-5363-5

S. Mitsch, K. Ghorbal, and A. Platzer, On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles, Robotics: Science and Systems IX, 2013.
DOI : 10.15607/RSS.2013.IX.014

S. Mitsch, S. Loos, and A. Platzer, Towards Formal Verification of Freeway Traffic Control, 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, 2012.
DOI : 10.1109/ICCPS.2012.25

S. Mitsch and A. Platzer, ModelPlex: verified runtime validation of verified cyber-physical system models, Formal Methods in System Design, vol.35, issue.6, pp.33-74, 2016.
DOI : 10.1109/TSMCB.2005.850178

A. Müller, S. Mitsch, W. Retschitzegger, W. Schwinger, and A. Platzer, A Component-Based Approach to Hybrid Systems Safety Verification, Integrated Formal Methods -12th International Conference, IFM 2016 Proceedings, pp.441-456, 2016.
DOI : 10.1145/2737166.2737167

J. Pan, L. Zhang, and D. Manocha, Collision-free and smooth trajectory computation in cluttered envi- ronments, 2012.

E. Plaku, L. Kavraki, and M. Vardi, Hybrid systems: from verification to falsification by??combining motion planning and discrete search, Formal Methods in System Design, vol.1, issue.7, pp.157-182, 2009.
DOI : 10.1007/11513988_3

E. Plaku, L. Kavraki, and M. Vardi, Falsification of LTL safety properties in hybrid systems, International Journal on Software Tools for Technology Transfer, vol.2, issue.3, pp.305-320, 2013.
DOI : 10.1007/3-540-44829-2_5

A. Platzer, Differential Dynamic Logic for Hybrid Systems, Journal of Automated Reasoning, vol.30, issue.1, pp.143-189, 2008.
DOI : 10.1007/978-1-4612-0601-9

A. Platzer, Logical analysis of hybrid systems: Proving theorems for complex dynamics, pp.978-981, 2010.

A. Platzer, Differential-algebraic Dynamic Logic for Differential-algebraic Programs, Journal of Logic and Computation, vol.20, issue.1, pp.309-352, 2010.
DOI : 10.1093/logcom/exn070

A. Platzer, Quantified differential dynamic logic for distributed hybrid systems Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Proceedings, pp.469-483, 2010.

A. Platzer, Stochastic differential dynamic logic for stochastic hybrid programs, LNCS, vol.6803, pp.431-445, 2011.

A. Platzer, Logics of Dynamical Systems, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.13-24, 2012.
DOI : 10.1109/LICS.2012.13

A. Platzer, The Complete Proof Theory of Hybrid Systems, 2012 27th Annual IEEE Symposium on Logic in Computer Science, 2012.
DOI : 10.1109/LICS.2012.64

A. Platzer, The Structure of Differential Invariants and Differential Cut Elimination, Logical Methods in Computer Science, vol.8, issue.4, pp.1-38, 2012.
DOI : 10.2168/LMCS-8(4:16)2012

A. Platzer, A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems Special issue for selected papers from CSL'10, Logical Methods in Computer Science, vol.8, issue.4, pp.1-44, 2012.

A. Platzer, Differential Game Logic, ACM Transactions on Computational Logic, vol.17, issue.1, pp.1-1, 2015.
DOI : 10.1007/978-1-4612-0601-9

A. Platzer, A Complete Uniform Substitution Calculus for Differential Dynamic Logic, Journal of Automated Reasoning, vol.89, issue.1, pp.219-26510, 2017.
DOI : 10.1007/978-1-4612-0601-9

A. Platzer and E. Clarke, Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study, LNCS, vol.5850, pp.547-562, 2009.
DOI : 10.1007/978-3-642-05089-3_35

A. Platzer and J. Quesel, KeYmaera: A hybrid theorem prover for hybrid systems, LNCS, vol.5195, pp.171-178, 2008.

J. Quesel, S. Mitsch, S. Loos, N. Aréchiga, and A. Platzer, How to model and prove hybrid systems with KeYmaera: a tutorial on safety, International Journal on Software Tools for Technology Transfer, vol.43, issue.4, pp.67-91, 2016.
DOI : 10.1007/978-3-540-71493-4_43

S. Sarid, B. Xu, and H. Kress-gazit, Guaranteeing highlevel behaviors while exploring partially known maps In: Robotics: Science and Systems VIII, 2012.

D. Seward, C. Pace, and R. Agate, Safe and effective navigation of autonomous robots in hazardous environments, Autonomous Robots, vol.70, issue.3, 2007.
DOI : 10.1007/s10514-006-9721-0

A. Sogokon, K. Ghorbal, P. Jackson, and A. Platzer, A Method for Invariant Generation for Polynomial Continuous Systems, In: Jobstmann B and Leino KRM, 2016.
DOI : 10.1007/978-3-662-49122-5_13

URL : https://hal.archives-ouvertes.fr/hal-01374902

H. Täubig, U. Frese, C. Hertzberg, C. Lüth, S. Mohr et al., Guaranteeing functional safety: design for provability and computer-aided verification, Autonomous Robots, vol.22, issue.12, pp.303-331, 2012.
DOI : 10.1177/0278364903022012002