{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:38:06Z","timestamp":1762508286787,"version":"3.37.3"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4-6","license":[{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"the National Key R & D Plan","award":["2019YFB1309900"],"award-info":[{"award-number":["2019YFB1309900"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61876111"],"award-info":[{"award-number":["61876111"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61602325"],"award-info":[{"award-number":["61602325"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61877040"],"award-info":[{"award-number":["61877040"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"the Project of Beijing Municipal Education Commission","award":["KM20190028005"],"award-info":[{"award-number":["KM20190028005"]}]},{"name":"Capacity Building for Sci-Tech Innovation - Fundamental Scientific Research Funds","award":["006195305000"],"award-info":[{"award-number":["006195305000"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2020,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Camera 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 \thave 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.<\/jats:p>","DOI":"10.1007\/s00165-020-00520-5","type":"journal-article","created":{"date-parts":[[2020,11,5]],"date-time":"2020-11-05T13:02:46Z","timestamp":1604581366000},"page":"417-437","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Formalization of Camera Pose Estimation Algorithm based on Rodrigues Formula"],"prefix":"10.1145","volume":"32","author":[{"given":"Shanyan","family":"Chen","sequence":"first","affiliation":[{"name":"Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing, China"},{"name":"School of Mathematical Science, Capital Normal University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3176-317X","authenticated-orcid":false,"given":"Guohui","family":"Wang","sequence":"additional","affiliation":[{"name":"Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing, China"},{"name":"School of Mathematical Science, Capital Normal University, Beijing, China"}]},{"given":"Ximeng","family":"Li","sequence":"additional","affiliation":[{"name":"Beijing Key Laboratory of Electronic System Reliability Technology, College of Information Engineering, Capital Normal University, Beijing, China"},{"name":"International Science and Technology Cooperation Base of Electronic System Reliability and Mathematical Interdisciplinary, Capital Normal University, Beijing, China"}]},{"given":"Qianying","family":"Zhang","sequence":"additional","affiliation":[{"name":"International Science and Technology Cooperation Base of Electronic System Reliability and Mathematical Interdisciplinary, Capital Normal University, Beijing, China"},{"name":"Beijing Advanced Innovation Center for Imaging Theory and Technology, Capital Normal University, Beijing, China"}]},{"given":"Zhiping","family":"Shi","sequence":"additional","affiliation":[{"name":"Beijing Key Laboratory of Electronic System Reliability Technology, College of Information Engineering, Capital Normal University, Beijing, China"},{"name":"International Science and Technology Cooperation Base of Electronic System Reliability and Mathematical Interdisciplinary, Capital Normal University, Beijing, China"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[{"name":"International Science and Technology Cooperation Base of Electronic System Reliability and Mathematical Interdisciplinary, Capital Normal University, Beijing, China"},{"name":"Beijing Advanced Innovation Center for Imaging Theory and Technology, Capital Normal University, Beijing, China"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Affeldt R Cohen C (2017) Formal foundations of 3d geometry to model robot manipulators. In: ACM Sigplan conference on certified programs and proofs pp 30\u201342","DOI":"10.1145\/3018610.3018629"},{"key":"e_1_2_1_2_2_2","volume-title":"Robotic manipulators and the product of exponentials formula","author":"Brockett RW","year":"1984","unstructured":"BrockettRWRobotic manipulators and the product of exponentials formula1984BerlinSpringer10.1007\/BFb0031048"},{"key":"e_1_2_1_2_3_2","first-page":"084","article-title":"A compact formula for rotations as spin matrix polynomials","volume":"10","author":"Curtright Thomas L","year":"2014","unstructured":"Curtright ThomasLFairlie DavidBZachos CosmasKA compact formula for rotations as spin matrix polynomialsHigh Energy Phys Div20141008432618601328.81124","journal-title":"High Energy Phys Div"},{"issue":"2","key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/s10851-012-0360-0","article-title":"A novel solution to the p4p problem for an uncalibrated camera","volume":"45","author":"Yang Guo","year":"2013","unstructured":"YangGuoA novel solution to the p4p problem for an uncalibrated cameraJ Math Imaging Vis2013452186198301740710.1007\/s10851-012-0360-0","journal-title":"J Math Imaging Vis"},{"issue":"11","key":"e_1_2_1_2_5_2","first-page":"1","article-title":"Formal proof\u2013theory and practice","volume":"55","author":"John Harrison","year":"2008","unstructured":"JohnHarrisonFormal proof\u2013theory and practiceNot Am Math Soc200855111224639921154.03303","journal-title":"Not Am Math Soc"},{"issue":"2","key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","article-title":"The HOL light theory of euclidean space","volume":"50","author":"John Harrison","year":"2013","unstructured":"JohnHarrisonThe HOL light theory of euclidean spaceJ Autom Reason2013502173190301680010.1007\/s10817-012-9250-9","journal-title":"J Autom Reason"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Hall B.C.: Lie groups lie algebras and representations. Springer (2013)","DOI":"10.1007\/978-1-4614-7116-5_16"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.006"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Khan S. Hasan O. Mashkoor A. (2018) Formal verification and safety assessment of a hemodialysis machine. SOFSEM : volume 10706 LNCS pp. 241\u2013254. Krems Austria (2018)","DOI":"10.1007\/978-3-319-73117-9_17"},{"key":"e_1_2_1_2_10_2","unstructured":"Li B Heng L Lee GH Pollefeys M (2013) A 4-point algorithm for relative pose estimation of a calibrated camera with a known relative rotation angle. In: IEEE\/RSJ international conference on intelligent robots and systems"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11263-008-0152-6"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Luvizon DC Picard D Tabia H (2018) 2d\/3d pose estimation and action recognition using multitask deep learning. In: Proceedings of the IEEE computer society conference on computer vision and pattern recognition. Salt Lake City UT United states pp 5137\u20135146","DOI":"10.1109\/CVPR.2018.00539"},{"key":"e_1_2_1_2_13_2","unstructured":"Murray R.M. Shankar S.S. Li Z.: A mathematical introduction to robotic manipulation. CRC Press Inc (1994)"},{"key":"e_1_2_1_2_14_2","unstructured":"Multivariable calculus libraries (2020) https:\/\/github.com\/jrh13\/hol-light\/tree\/master\/Multivariate"},{"key":"e_1_2_1_2_15_2","first-page":"45","article-title":"Markerless camera pose estimation\u2013an overview","volume":"19","author":"Noll T","year":"2010","unstructured":"NollTPaganiAStrickerDMarkerless camera pose estimation\u2013an overviewOpenAccess Ser Inf2010194554","journal-title":"OpenAccess Ser Inf"},{"key":"e_1_2_1_2_16_2","unstructured":"Peng C (2017) An iterative camera pose estimation algorithm based on epnp. In: Chinese intelligent automation conference"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Pavllo D Feichtenhofer C Grangier D Auli M (2018) 3d human pose estimation in video with temporal convolutions and semi-supervised training","DOI":"10.1109\/CVPR.2019.00794"},{"key":"e_1_2_1_2_18_2","unstructured":"Projections onto subspaces (2011). https:\/\/ocw.mit.edu\/courses\/mathematics\/18-06sc-linear-algebra-fall-2011\/least-squares-determinants-and-eigenvalues\/projections-onto-subspaces\/MIT18_06SCF11_Ses2.2sum.pdf"},{"key":"e_1_2_1_2_19_2","unstructured":"Rashid A Hasan O (2018) Formal modeling of robotic cell injection systems in higher-order logic. In: CEUR workshop proceedings vol 2307 Hagenberg Austria"},{"key":"e_1_2_1_2_20_2","volume-title":"Elements of vector analysis","author":"Roy KK","year":"2008","unstructured":"RoyKKElements of vector analysis2008BerlinSpringer10.1007\/978-3-540-72334-9_1"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Sun C. Dong H. Zhang B. Wang P.: An orthogonal iteration pose estimation algorithm based on an incident ray tracking model. Meas Sci Technol 29 (9) (2018)","DOI":"10.1088\/1361-6501\/aad014"},{"key":"e_1_2_1_2_22_2","first-page":"13","article-title":"Aas 95\u2013137 stereographic orientation parameters for attitude dynamics: a generalization of the rodrigues parameters","volume":"44","author":"Schaub H","year":"1996","unstructured":"SchaubHJunkinsJLAas 95\u2013137 stereographic orientation parameters for attitude dynamics: a generalization of the rodrigues parametersJ Astron Sci1996441315","journal-title":"J Astron Sci"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Schaub H Tsiotras P Junkins JL (1995) Principal rotation representations of proper nxn orthogonal matrices. Int J Eng Sci 33(15):2277\u20132295. The Edelen Symposium","DOI":"10.1016\/0020-7225(95)00070-E"},{"key":"e_1_2_1_2_24_2","first-page":"2033","volume-title":"The solution distribution analysis of the p3p problem","author":"Sun F","year":"2010","unstructured":"SunFWangBThe solution distribution analysis of the p3p problem2010TurkeyIstanbul20332036"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Shi Z Yan Z Liu Z Kang X Yong G Jie Z Song X (2014) Formalization of matrix theory in hol4. Adv Mech Eng (2014-8-28) 2014:195276\u2013195276","DOI":"10.1155\/2014\/195276"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.amc.2008.05.037"},{"key":"e_1_2_1_2_27_2","first-page":"1","article-title":"Modified rodrigues parameters: an efficient representation of orientation in 3d vision and graphics","volume":"2","author":"Terzakis G","year":"2017","unstructured":"TerzakisGLourakisMAit-BoudaoudDModified rodrigues parameters: an efficient representation of orientation in 3d vision and graphicsJ Math Imaging Vis201721211433.68471","journal-title":"J Math Imaging Vis"},{"key":"e_1_2_1_2_28_2","unstructured":"Zhao Z (2014) Research on videometrics technology in the aircraft transformation collision avoidance system. Master thesis National University of Defense Technology"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00520-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-020-00520-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00520-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-020-00520-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T17:48:43Z","timestamp":1649180923000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-020-00520-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11]]},"references-count":28,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2020,11]]}},"alternative-id":["10.1007\/s00165-020-00520-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-020-00520-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2020,11]]},"assertion":[{"value":"31 October 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 September 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 November 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}