TY  - JOUR
AU  - Martin-Martin, Enrique
AU  - Montenegro Montes, Manuel
AU  - Riesco Rodríguez, Adrián
AU  - Rodríguez Hortalá, Juan
AU  - Rubio Cuéllar, Rubén Rafael
PY  - 2023
DO  - 10.1016/j.jlamp.2023.100860
SN  - 2352-2216
UR  - https://hdl.handle.net/20.500.14352/73028
T2  - Journal of Logical and Algebraic Methods in Programming
AB  - The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The Navigation Stack stands out among the different libraries available in ROS, providing a set of components that can be reused...
LA  - spa
M2  - 100860
PB  - Elsevier
KW  - Formal verification
KW  - Model checking
KW  - ROS
KW  - Maude
KW  - Navigation
KW  - Dafny
TI  - Verification of the ROS NavFn planner using executable specification languages
TY  - journal article
VL  - 132
ER  -