Name
Abstract | ||
|---|---|---|
AbstractAbstractCamera pose estimation is key to the proper functioning of robotic systems, supporting critical tasks such as robot navigation, target tracking, camera calibration, etc.Whilemultiple algorithms solving this problem have been proposed, their correctness has rarely been validated using formal techniques. This is true despite the fact that the adoption of formal verification is essential for the reliability of safety-critical systems, and for their certification to high assurance levels. In this article, we present an effort in formally verifying an algorithm for camera pose estimation in an interactive theorem prover. The algorithm leverages the power of Rodrigues formula to solve the pose estimation problem under conditions for which existing solutions cannot be applied. The technical ingredients include (but are not limited to) mechanized proofs of the Rodrigues formula (along with its Cayley decomposition form) and the least squares method for fitting data. Based on the formalization of the algorithm, we formally derive and verify its general solution and unique solution. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/s00165-020-00520-5 | Formal Aspects of Computing |
Keywords | DocType | Volume |
Camera pose estimation, Rodrigues formula, Least squares method, Formalization, HOL Light | Journal | 32 |
Issue | ISSN | Citations |
4-6 | 0934-5043 | 0 |
PageRank | References | Authors |
0.34 | 12 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shanyan Chen | 1 | 0 | 0.34 |
| Guohui Wang | 2 | 0 | 3.04 |
| Ximeng Li | 3 | 10 | 5.27 |
| Qianying Zhang | 4 | 10 | 4.91 |
| Zhiping Shi | 5 | 168 | 43.86 |
| Yong Guan | 6 | 787 | 82.67 |