Static Analysis Techniques for Robotics Software Verification

Abstract-- We overview the main semantics-based static analysis techniques for software verification: Data-flow analysis, Control-flow Analysis, Model Checking, and Abstract Interpretation. The complexity of control software, lying at the core of robotic systems, and the intensive use of numeric values pose several challenges for the formal verification of either functional or non-functional properties. Index Terms—Static Analysis, Formal Verification