Verification of the ROS NavFn planner using executable specification languages

DOI10.1016/J.JLAMP.2023.100860OpenAlexW4320712511MaRDI QIDQ2693303

Enrique Martin-Martin, Manuel Montenegro, Adrián Riesco, Rubén Rubio, Juan Rodríguez-Hortalá

Publication date: 20 March 2023

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2023.100860

zbMATH Keywords

navigationformal verificationmodel checkingMaudeROSDafny

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• Coq
• Dafny
• KeY-C
• Isabelle/HOL
• Frama-C
• Maude
• ITP
• Lean
• ROS
• ROSMonitoring
• Marathon 2
• DeepXplore
• CRADLE

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Conditional rewriting logic as a unified model of concurrency
• Isabelle/HOL. A proof assistant for higher-order logic
• Specification and proof in membership equational logic
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
• Strategies, model checking and branching-time properties in Maude
• Programming and symbolic computation in Maude
• A mechanized semantics for C++ object construction and destruction, with applications to resource management
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• Dafny: An Automatic Program Verifier for Functional Correctness
• The Lean Theorem Prover (System Description)

This page was built for publication: Verification of the ROS NavFn planner using executable specification languages