Graph-based SLAM has proved to be one of the most effective solutions to the Simultaneous localization and Mapping problem. This approach relies on nonlinear iterative optimization methods that in practice perform both
accurately and efficiently. However, due to the non-convexity of the problem, the obtained solutions come with no guarantee of global optimality and may get stuck in local minima. The
application of SLAM to many real-world applications cannot be conceived without additional control tools that detect possible
suboptimalities as soon as possible in order to take corrective action and avoid catastrophic failure of the entire system.
This paper builds upon the state-of-the-art framework  in verification for this problem and introduces a novel superior formulation that leads to a much higher efficiency. While
retaining the same high effectiveness, the verification times of our proposal reduce up to >50x, paving the way for faster verification in critical real applications or in embedded low-power systems.We support our claims with extensive experiments with real and simulated data.